------------------------------------------------------------------------
-- 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