Equality on dependent function types
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.
Created on 2022-01-31.
Last modified on 2023-09-26.
module foundation.equality-dependent-function-types where
Imports
open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.type-theoretic-principle-of-choice open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.functoriality-dependent-function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types
Idea
Given a family of types B
over A
, if we can characterize the
identity types of each B x
, then we can
characterize the identity types of (x : A) → B x
.
Contractibility
is-contr-total-Eq-Π : { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) → ( is-contr-total-C : (x : A) → is-contr (Σ (B x) (C x))) → is-contr (Σ ((x : A) → B x) (λ g → (x : A) → C x (g x))) is-contr-total-Eq-Π {A = A} {B} C is-contr-total-C = is-contr-equiv' ( (x : A) → Σ (B x) (C x)) ( distributive-Π-Σ) ( is-contr-Π is-contr-total-C) is-contr-total-Eq-implicit-Π : { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (C : (x : A) → B x → UU l3) → ( is-contr-total-C : (x : A) → is-contr (Σ (B x) (C x))) → is-contr (Σ ({x : A} → B x) (λ g → {x : A} → C x (g {x}))) is-contr-total-Eq-implicit-Π {A = A} {B} C is-contr-total-C = is-contr-equiv ( Σ ((x : A) → B x) (λ g → (x : A) → C x (g x))) ( equiv-Σ ( λ g → (x : A) → C x (g x)) ( equiv-explicit-implicit-Π) ( λ _ → equiv-explicit-implicit-Π)) ( is-contr-total-Eq-Π C is-contr-total-C)
Extensionality
module _ {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) (Eq-B : (x : A) → B x → UU l3) where map-extensionality-Π : ( (x : A) (y : B x) → (f x = y) ≃ Eq-B x y) → ( g : (x : A) → B x) → f = g → ((x : A) → Eq-B x (g x)) map-extensionality-Π e .f refl x = map-equiv (e x (f x)) refl abstract is-equiv-map-extensionality-Π : (e : (x : A) (y : B x) → (f x = y) ≃ Eq-B x y) → (g : (x : A) → B x) → is-equiv (map-extensionality-Π e g) is-equiv-map-extensionality-Π e = fundamental-theorem-id ( is-contr-total-Eq-Π Eq-B ( λ x → fundamental-theorem-id' ( λ y → map-equiv (e x y)) ( λ y → is-equiv-map-equiv (e x y)))) ( map-extensionality-Π e) extensionality-Π : ( (x : A) (y : B x) → (f x = y) ≃ Eq-B x y) → ( g : (x : A) → B x) → (f = g) ≃ ((x : A) → Eq-B x (g x)) pr1 (extensionality-Π e g) = map-extensionality-Π e g pr2 (extensionality-Π e g) = is-equiv-map-extensionality-Π e g
See also
-
Equality proofs in the fiber of a map are characterized in
foundation.equality-fibers-of-maps
. -
Equality proofs in cartesian product types are characterized in
foundation.equality-cartesian-product-types
. -
Equality proofs in dependent pair types are characterized in
foundation.equality-dependent-pair-types
. -
Function extensionality is postulated in
foundation.function-extensionality
.
Recent changes
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).