Equality of dependent pair types
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.
Created on 2022-02-07.
Last modified on 2023-09-11.
module foundation-core.equality-dependent-pair-types where
Imports
open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.dependent-identifications open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.transport-along-identifications
Idea
An identification (pair x y) = (pair x' y')
in a dependent pair type Σ A B
is equivalently described as a pair pair α β
consisting of an identification
α : x = x'
and an identification β : (tr B α y) = y'
.
Definition
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where Eq-Σ : (s t : Σ A B) → UU (l1 ⊔ l2) Eq-Σ s t = Σ (pr1 s = pr1 t) (λ α → dependent-identification B α (pr2 s) (pr2 t))
Properties
The type Id s t
is equivalent to Eq-Σ s t
for any s t : Σ A B
refl-Eq-Σ : (s : Σ A B) → Eq-Σ s s pr1 (refl-Eq-Σ (pair a b)) = refl pr2 (refl-Eq-Σ (pair a b)) = refl pair-eq-Σ : {s t : Σ A B} → s = t → Eq-Σ s t pair-eq-Σ {s} refl = refl-Eq-Σ s eq-pair-Σ : {s t : Σ A B} (α : pr1 s = pr1 t) → dependent-identification B α (pr2 s) (pr2 t) → s = t eq-pair-Σ {pair x y} {pair .x .y} refl refl = refl eq-pair-Σ' : {s t : Σ A B} → Eq-Σ s t → s = t eq-pair-Σ' p = eq-pair-Σ (pr1 p) (pr2 p) is-retraction-pair-eq-Σ : (s t : Σ A B) → ((pair-eq-Σ {s} {t}) ∘ (eq-pair-Σ' {s} {t})) ~ id {A = Eq-Σ s t} is-retraction-pair-eq-Σ (pair x y) (pair .x .y) (pair refl refl) = refl is-section-pair-eq-Σ : (s t : Σ A B) → ((eq-pair-Σ' {s} {t}) ∘ (pair-eq-Σ {s} {t})) ~ id is-section-pair-eq-Σ (pair x y) .(pair x y) refl = refl abstract is-equiv-eq-pair-Σ : (s t : Σ A B) → is-equiv (eq-pair-Σ' {s} {t}) is-equiv-eq-pair-Σ s t = is-equiv-is-invertible ( pair-eq-Σ) ( is-section-pair-eq-Σ s t) ( is-retraction-pair-eq-Σ s t) equiv-eq-pair-Σ : (s t : Σ A B) → Eq-Σ s t ≃ (s = t) equiv-eq-pair-Σ s t = pair eq-pair-Σ' (is-equiv-eq-pair-Σ s t) abstract is-equiv-pair-eq-Σ : (s t : Σ A B) → is-equiv (pair-eq-Σ {s} {t}) is-equiv-pair-eq-Σ s t = is-equiv-is-invertible ( eq-pair-Σ') ( is-retraction-pair-eq-Σ s t) ( is-section-pair-eq-Σ s t) equiv-pair-eq-Σ : (s t : Σ A B) → (s = t) ≃ Eq-Σ s t equiv-pair-eq-Σ s t = pair pair-eq-Σ (is-equiv-pair-eq-Σ s t) η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) = t η-pair t = eq-pair-Σ refl refl
Lifting equality to the total space
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where lift-eq-Σ : {x y : A} (p : x = y) (b : B x) → (pair x b) = (pair y (tr B p b)) lift-eq-Σ refl b = refl
Transport in a family of dependent pair types
tr-Σ : {l1 l2 l3 : Level} {A : UU l1} {a0 a1 : A} {B : A → UU l2} (C : (x : A) → B x → UU l3) (p : a0 = a1) (z : Σ (B a0) (λ x → C a0 x)) → tr (λ a → (Σ (B a) (C a))) p z = pair (tr B p (pr1 z)) (tr (ind-Σ C) (eq-pair-Σ p refl) (pr2 z)) tr-Σ C refl z = refl
Transport in a family over a dependent pair type
tr-eq-pair-Σ : {l1 l2 l3 : Level} {A : UU l1} {a0 a1 : A} {B : A → UU l2} {b0 : B a0} {b1 : B a1} (C : (Σ A B) → UU l3) (p : a0 = a1) (q : dependent-identification B p b0 b1) (u : C (a0 , b0)) → tr C (eq-pair-Σ p q) u = tr (λ x → C (a1 , x)) q (tr C (eq-pair-Σ p refl) u) tr-eq-pair-Σ C refl refl u = refl
See also
- Equality proofs in cartesian product types are characterized in
foundation.equality-cartesian-product-types
. - Equality proofs in dependent function types are characterized in
foundation.equality-dependent-function-types
. - Equality proofs in the fiber of a map are characterized in
foundation.equality-fibers-of-maps
.
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-11. Egbert Rijke. complete refactoring of dependent identifications (#653).