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

Idea

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

Examples

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

_∘_ :
  {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

• Postcomposition
• Precomposition

Table of files about function types, composition, and equivalences

Recent changes

• 2024-01-28. Fredrik Bakke. Equivalence injective type families (#1009).
• 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
• 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
• 2023-09-10. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).
• 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).