Function types
Content created by Egbert Rijke, Fredrik Bakke, Vojtěch Štěpančík and Raymond Baker.
Created on 2023-06-10.
Last modified on 2023-12-05.
module foundation.function-types where open import foundation-core.function-types public
Imports
open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.homotopy-induction open import foundation.universe-levels open import foundation-core.dependent-identifications open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.transport-along-identifications
Properties
Transport in a family of function types
module _ {l1 l2 l3 : Level} {A : UU l1} {x y : A} (B : A → UU l2) (C : A → UU l3) where tr-function-type : (p : x = y) (f : B x → C x) → tr (λ a → B a → C a) p f = (tr C p ∘ (f ∘ tr B (inv p))) tr-function-type refl f = refl compute-dependent-identification-function-type : (p : x = y) (f : B x → C x) (g : B y → C y) → ((b : B x) → tr C p (f b) = g (tr B p b)) ≃ (tr (λ a → B a → C a) p f = g) compute-dependent-identification-function-type refl f g = inv-equiv equiv-funext map-compute-dependent-identification-function-type : (p : x = y) (f : B x → C x) (g : B y → C y) → ((b : B x) → tr C p (f b) = g (tr B p b)) → (tr (λ a → B a → C a) p f = g) map-compute-dependent-identification-function-type p f g = map-equiv (compute-dependent-identification-function-type p f g)
Relation between compute-dependent-identification-function-type
and preserves-tr
module _ {l1 l2 l3 : Level} {I : UU l1} {i0 i1 : I} {A : I → UU l2} {B : I → UU l3} (f : (i : I) → A i → B i) where preserves-tr-apd-function : (p : i0 = i1) (a : A i0) → map-inv-equiv ( compute-dependent-identification-function-type A B p (f i0) (f i1)) ( apd f p) a = inv-htpy (preserves-tr f p) a preserves-tr-apd-function refl = refl-htpy
Computation of dependent identifications of functions over homotopies
module _ { l1 l2 l3 l4 : Level} { S : UU l1} {X : UU l2} {P : X → UU l3} (Y : UU l4) { i : S → X} where equiv-htpy-dependent-function-dependent-identification-function-type : { j : S → X} (H : i ~ j) → ( k : (s : S) → P (i s) → Y) ( l : (s : S) → P (j s) → Y) → ( s : S) → ( k s ~ (l s ∘ tr P (H s))) ≃ ( dependent-identification ( λ x → P x → Y) ( H s) ( k s) ( l s)) equiv-htpy-dependent-function-dependent-identification-function-type = ind-htpy i ( λ j H → ( k : (s : S) → P (i s) → Y) → ( l : (s : S) → P (j s) → Y) → ( s : S) → ( k s ~ (l s ∘ tr P (H s))) ≃ ( dependent-identification ( λ x → P x → Y) ( H s) ( k s) ( l s))) ( λ k l s → inv-equiv (equiv-funext)) compute-equiv-htpy-dependent-function-dependent-identification-function-type : { j : S → X} (H : i ~ j) → ( h : (x : X) → P x → Y) → ( s : S) → ( map-equiv ( equiv-htpy-dependent-function-dependent-identification-function-type H ( h ∘ i) ( h ∘ j) ( s)) ( λ t → ap (ind-Σ h) (eq-pair-Σ (H s) refl))) = ( apd h (H s)) compute-equiv-htpy-dependent-function-dependent-identification-function-type = ind-htpy i ( λ j H → ( h : (x : X) → P x → Y) → ( s : S) → ( map-equiv ( equiv-htpy-dependent-function-dependent-identification-function-type ( H) ( h ∘ i) ( h ∘ j) ( s)) ( λ t → ap (ind-Σ h) (eq-pair-Σ (H s) refl))) = ( apd h (H s))) ( λ h s → ( ap ( λ f → map-equiv (f (h ∘ i) (h ∘ i) s) refl-htpy) ( compute-ind-htpy i ( λ j H → ( k : (s : S) → P (i s) → Y) → ( l : (s : S) → P (j s) → Y) → ( s : S) → ( k s ~ (l s ∘ tr P (H s))) ≃ ( dependent-identification ( λ x → P x → Y) ( H s) ( k s) ( l s))) ( λ k l s → inv-equiv (equiv-funext)))) ∙ ( eq-htpy-refl-htpy (h (i s))))
Composing families of functions
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3} {D : A → UU l4} where dependent-comp : ((a : A) → C a → D a) → ((a : A) → B a → C a) → (a : A) → B a → D a dependent-comp g f a b = g a (f a b)
See also
Table of files about function types, composition, and equivalences
Recent changes
- 2023-12-05. Raymond Baker and Egbert Rijke. Universal property of fibers (#944).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-10-10. Vojtěch Štěpančík and Egbert Rijke. Flattening lemma for pushouts 2: descent data boogaloo (#816).
- 2023-09-15. Fredrik Bakke. Define representations of monoids (#765).
- 2023-09-13. Vojtěch Štěpančík. Flattening lemma for pushouts (#764).