------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for Functions
------------------------------------------------------------------------
 
-- The contents of this file should always be accessed from `Function`.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Function.Core where
 
open import Level using (_⊔_)
 
------------------------------------------------------------------------
-- Types
 
Fun₁ : ∀ {a} → Set a → Set a
Fun₁ A = A → A
 
Fun₂ : ∀ {a} → Set a → Set a
Fun₂ A = A → A → A
 
------------------------------------------------------------------------
-- Morphism
 
Morphism : ∀ {a} → ∀ {b} → Set a → Set b → Set (a ⊔ b)
Morphism A B = A → B