Equality of dependent pair types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Eléonore Mangel, Vojtěch Štěpančík, Julian KG, fernabnor, louismntnu and maybemabeline.

Created on 2022-01-26.

module foundation.equality-dependent-pair-types where

open import foundation-core.equality-dependent-pair-types public

Imports
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-identifications
open import foundation.dependent-pair-types
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types


Idea

The operation eq-pair-Σ can be seen as a "vertical composition" operation that combines an identification and a dependent identification over it into a single identification. This operation preserves, in the appropriate sense, the groupoidal structure on dependent identifications.

Properties

Interchange law of concatenation and eq-pair-Σ

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
where

interchange-concat-eq-pair-Σ :
{x y z : A} (p : x ＝ y) (q : y ＝ z) {x' : B x} {y' : B y} {z' : B z} →
(p' : dependent-identification B p x' y')
(q' : dependent-identification B q y' z') →
eq-pair-Σ (p ∙ q) (concat-dependent-identification B p q p' q') ＝
( eq-pair-Σ p p' ∙ eq-pair-Σ q q')
interchange-concat-eq-pair-Σ refl q refl q' = refl


Interchange law for concatenation and pair-eq-Σ

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
where

interchange-concat-pair-eq-Σ :
{x y z : Σ A B} (p : x ＝ y) (q : y ＝ z) →
pair-eq-Σ (p ∙ q) ＝
( pr1 (pair-eq-Σ p) ∙ pr1 (pair-eq-Σ q) ,
concat-dependent-identification B
( pr1 (pair-eq-Σ p))
( pr1 (pair-eq-Σ q))
( pr2 (pair-eq-Σ p))
( pr2 (pair-eq-Σ q)))
interchange-concat-pair-eq-Σ refl q = refl

pr1-interchange-concat-pair-eq-Σ :
{x y z : Σ A B} (p : x ＝ y) (q : y ＝ z) →
pr1 (pair-eq-Σ (p ∙ q)) ＝ (pr1 (pair-eq-Σ p) ∙ pr1 (pair-eq-Σ q))
pr1-interchange-concat-pair-eq-Σ p q =
ap pr1 (interchange-concat-pair-eq-Σ p q)


Distributivity of inv over eq-pair-Σ

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
where

distributive-inv-eq-pair-Σ :
{x y : A} (p : x ＝ y) {x' : B x} {y' : B y}
(p' : dependent-identification B p x' y') →
inv (eq-pair-Σ p p') ＝
eq-pair-Σ (inv p) (inv-dependent-identification B p p')
distributive-inv-eq-pair-Σ refl refl = refl

distributive-inv-eq-pair-Σ-refl :
{x : A} {x' y' : B x} (p' : x' ＝ y') →
inv (eq-pair-eq-fiber p') ＝ eq-pair-Σ {A = A} {B = B} refl (inv p')
distributive-inv-eq-pair-Σ-refl refl = refl


Computing pair-eq-Σ at an identification of the form ap f p

module _
{l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : A → UU l3} (f : X → Σ A B)
where

pair-eq-Σ-ap :
{x y : X} (p : x ＝ y) →
pair-eq-Σ (ap f p) ＝
( ( ap (pr1 ∘ f) p) ,
( substitution-law-tr B (pr1 ∘ f) p ∙ apd (pr2 ∘ f) p))
pair-eq-Σ-ap refl = refl

pr1-pair-eq-Σ-ap :
{x y : X} (p : x ＝ y) →
pr1 (pair-eq-Σ (ap f p)) ＝ ap (pr1 ∘ f) p
pr1-pair-eq-Σ-ap refl = refl


Computing action of functions on identifications of the form eq-pair-Σ p q

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y)
where

compute-ap-eq-pair-Σ :
{ x y : A} (p : x ＝ y) {b : B x} {b' : B y} →
( q : dependent-identification B p b b') →
ap f (eq-pair-Σ p q) ＝ (ap f (eq-pair-Σ p refl) ∙ ap (ev-pair f y) q)
compute-ap-eq-pair-Σ refl refl = refl


Equality of dependent pair types consists of two orthogonal components

module _
{l1 l2 : Level} {A : UU l1} (B : A → UU l2)
where

triangle-eq-pair-Σ :
{ a a' : A} (p : a ＝ a') →
{ b : B a} {b' : B a'} (q : dependent-identification B p b b') →
eq-pair-Σ p q ＝ (eq-pair-Σ p refl ∙ eq-pair-Σ refl q)
triangle-eq-pair-Σ refl q = refl


Computing identifications in iterated dependent pair types

Computing identifications in dependent pair types of the form Σ (Σ A B) C

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3}
where

Eq-Σ²' : (s t : Σ (Σ A B) C) → UU (l1 ⊔ l2 ⊔ l3)
Eq-Σ²' s t =
Σ ( Eq-Σ (pr1 s) (pr1 t))
( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t))

equiv-triple-eq-Σ' :
(s t : Σ (Σ A B) C) →
(s ＝ t) ≃ Eq-Σ²' s t
equiv-triple-eq-Σ' s t =
( equiv-Σ
( λ q →
( dependent-identification
( C)
( eq-pair-Σ' q)
( pr2 s)
( pr2 t)))
( equiv-pair-eq-Σ (pr1 s) (pr1 t))
( λ p →
( equiv-tr
( λ q → dependent-identification C q (pr2 s) (pr2 t))
( inv (is-section-pair-eq-Σ (pr1 s) (pr1 t) p))))) ∘e
( equiv-pair-eq-Σ s t)

triple-eq-Σ' :
(s t : Σ (Σ A B) C) →
(s ＝ t) → Eq-Σ²' s t
triple-eq-Σ' s t = map-equiv (equiv-triple-eq-Σ' s t)


Computing dependent identifications on the second component

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
where

coh-eq-base-Σ² :
{s t : Σ A (λ x → Σ (B x) λ y → C x y)} (p : s ＝ t) →
eq-base-eq-pair-Σ p ＝
eq-base-eq-pair-Σ (eq-base-eq-pair-Σ (ap (map-inv-associative-Σ' A B C) p))
coh-eq-base-Σ² refl = refl

dependent-eq-second-component-eq-Σ² :
{s t : Σ A (λ x → Σ (B x) λ y → C x y)} (p : s ＝ t) →
dependent-identification B (eq-base-eq-pair-Σ p) (pr1 (pr2 s)) (pr1 (pr2 t))
dependent-eq-second-component-eq-Σ² {s = s} {t = t} p =
( ap (λ q → tr B q (pr1 (pr2 s))) (coh-eq-base-Σ² p)) ∙
( pr2
( pr1
( triple-eq-Σ'
( map-inv-associative-Σ' A B C s)
( map-inv-associative-Σ' A B C t)
( ap (map-inv-associative-Σ' A B C) p))))


Computing dependent identifications on the third component

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
(D : (x : A) → B x → C x → UU l4)
where

coh-eq-base-Σ³ :
{ s t : Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y)))} (p : s ＝ t) →
eq-base-eq-pair-Σ p ＝
eq-base-eq-pair-Σ (ap (map-equiv (interchange-Σ-Σ-Σ D)) p)
coh-eq-base-Σ³ refl = refl

dependent-eq-third-component-eq-Σ³ :
{ s t : Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y)))} (p : s ＝ t) →
dependent-identification C
( eq-base-eq-pair-Σ p)
( pr1 (pr2 (pr2 s)))
( pr1 (pr2 (pr2 t)))
dependent-eq-third-component-eq-Σ³ {s = s} {t = t} p =
( ap (λ q → tr C q (pr1 (pr2 (pr2 s)))) (coh-eq-base-Σ³ p)) ∙
( dependent-eq-second-component-eq-Σ²
( ap (map-equiv (interchange-Σ-Σ-Σ D)) p))