# Function types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-10.

module foundation-core.function-types where

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


### Table of files about function types, composition, and equivalences

ConceptFile
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
Equivalencesfoundation.equivalences
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
Postcompositionfoundation.postcomposition
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