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