------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for Functions
------------------------------------------------------------------------

-- The contents of this file should usually 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