Function types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-10.
Last modified on 2024-01-28.

module foundation-core.function-types where
open import foundation.universe-levels


Functions are primitive in Agda. Here we construct some basic functions


The identity function

id : {l : Level} {A : UU l}  A  A
id a = a

idω : {A : UUω}  A  A
idω a = a

Dependent composition of functions

infixr 15 _∘_

_∘_ :
  {l1 l2 l3 : Level} {A : UU l1} {B : A  UU l2} {C : (a : A)  B a  UU l3} 
  ({a : A}  (b : B a)  C a b)  (f : (a : A)  B a)  (a : A)  C a (f a)
(g  f) a = g (f a)

Evaluation at a point

ev-point :
  {l1 l2 : Level} {A : UU l1} (a : A) {P : A  UU l2}  ((x : A)  P x)  P a
ev-point a f = f a

ev-point' :
  {l1 l2 : Level} {A : UU l1} (a : A) {X : UU l2}  (A  X)  X
ev-point' a f = f a

Postcomposition functions

map-Π :
  {l1 l2 l3 : Level}
  {I : UU l1} {A : I  UU l2} {B : I  UU l3}
  (f : (i : I)  A i  B i) 
  ((i : I)  A i) 
  ((i : I)  B i)
map-Π f h i = f i (h i)

map-Π' :
  {l1 l2 l3 l4 : Level}
  {I : UU l1} {A : I  UU l2} {B : I  UU l3}
  {J : UU l4} (α : J  I) 
  ((i : I)  A i  B i) 
  ((j : J)  A (α j)) 
  ((j : J)  B (α j))
map-Π' α f = map-Π (f  α)

map-implicit-Π :
  {l1 l2 l3 : Level}
  {I : UU l1} {A : I  UU l2} {B : I  UU l3}
  (f : (i : I)  A i  B i) 
  ({i : I}  A i) 
  ({i : I}  B i)
map-implicit-Π f h {i} = map-Π f  i  h {i}) i

See also

Table of files about function types, composition, and equivalences

Decidable dependent function typesfoundation.decidable-dependent-function-types
Dependent universal property of equivalencesfoundation.dependent-universal-property-equivalences
Descent for equivalencesfoundation.descent-equivalences
Equivalence extensionalityfoundation.equivalence-extensionality
Equivalence inductionfoundation.equivalence-induction
Equivalences (foundation-core)foundation-core.equivalences
Families of equivalencesfoundation.families-of-equivalences
Fibered equivalencesfoundation.fibered-equivalences
Function extensionalityfoundation.function-extensionality
Function typesfoundation.function-types
Function types (foundation-core)foundation-core.function-types
Functional correspondencesfoundation.functional-corresponcences
Functoriality of dependent function typesfoundation.functoriality-dependent-function-types
Functoriality of dependent function types (foundation-core)foundation-core.functoriality-dependent-function-types
Functoriality of function typesfoundation.functoriality-function-types
Implicit function typesfoundation.implicit-function-types
Iterating functionsfoundation.iterating-functions
Precomposition of dependent functionsfoundation.precomposition-dependent-functions
Precomposition of dependent functions (foundation-core)foundation-core.precomposition-dependent-functions
Precomposition of functionsfoundation.precomposition-functions
Precomposition of functions (foundation-core)foundation-core.precomposition-functions
Precomposition of functions into subuniversesfoundation.precomposition-functions-into-subuniverses
Type arithmetic of dependent function typesfoundation.type-arithmetic-dependent-function-types
Univalence implies function extensionalityfoundation.univalence-implies-function-extensionality
Universal property of equivalencesfoundation.universal-property-equivalences
Weak function extensionalityfoundation.weak-function-extensionality

Recent changes