Equality in iterated Sigma types

src/foundation-core/equality-dependent-pair-types.lagda.md

@@ -109,13 +109,13 @@ module _
   η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
   η-pair t = refl
 
-  eq-base-eq-pair : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t)
-  eq-base-eq-pair p = pr1 (pair-eq-Σ p)
+  eq-base-eq-pair-Σ : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t)
+  eq-base-eq-pair-Σ p = pr1 (pair-eq-Σ p)
 
-  dependent-eq-family-eq-pair :
+  dependent-eq-family-eq-pair-Σ :
     {s t : Σ A B} → (p : s ＝ t) →
-    dependent-identification B (eq-base-eq-pair p) (pr2 s) (pr2 t)
-  dependent-eq-family-eq-pair p = pr2 (pair-eq-Σ p)
+    dependent-identification B (eq-base-eq-pair-Σ p) (pr2 s) (pr2 t)
+  dependent-eq-family-eq-pair-Σ p = pr2 (pair-eq-Σ p)
 ```
 
 ### Lifting equality to the total space

src/foundation-core/equivalences.lagda.md

@@ -588,6 +588,10 @@ module _
     (e : A ≃ B) (x y : A) → (x ＝ y) ≃ (map-equiv e x ＝ map-equiv e y)
   pr1 (equiv-ap e x y) = ap (map-equiv e)
   pr2 (equiv-ap e x y) = is-emb-is-equiv (is-equiv-map-equiv e) x y
+
+  map-inv-equiv-ap :
+    (e : A ≃ B) (x y : A) → (map-equiv e x ＝ map-equiv e y) → (x ＝ y)
+  map-inv-equiv-ap e x y = map-inv-equiv (equiv-ap e x y)
 ```
 
 ## Equivalence reasoning

src/foundation/equality-dependent-pair-types.lagda.md

@@ -11,9 +11,15 @@ open import foundation-core.equality-dependent-pair-types public
 ```agda
 open import foundation.action-on-identifications-dependent-functions
 open import foundation.action-on-identifications-functions
+open import foundation.contractible-types
 open import foundation.dependent-identifications
 open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
 open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.function-types
@@ -113,7 +119,7 @@ module _
 
 ```agda
 module _
-  { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y)
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {Y : UU l3} (f : Σ A B → Y)
   where
 
   compute-ap-eq-pair-Σ :
@@ -127,7 +133,7 @@ module _
 
 ```agda
 module _
-  { l1 l2 : Level} {A : UU l1} (B : A → UU l2)
+  {l1 l2 : Level} {A : UU l1} (B : A → UU l2)
   where
 
   triangle-eq-pair-Σ :
@@ -137,6 +143,96 @@ module _
   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
+
+```agda
+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
+
+```agda
+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
+
+```agda
+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))
+```
+
 ## See also
 
 - Equality proofs in cartesian product types are characterized in

src/foundation/type-arithmetic-dependent-pair-types.lagda.md

@@ -305,6 +305,14 @@ module _
   pr1 interchange-Σ-Σ = map-interchange-Σ-Σ
   pr2 interchange-Σ-Σ = is-equiv-map-interchange-Σ-Σ
 
+  interchange-Σ-Σ-Σ :
+    Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y))) ≃
+    Σ A (λ x → Σ (C x) (λ z → Σ (B x) λ y → D x y z))
+  interchange-Σ-Σ-Σ =
+    associative-Σ' A C (λ x z → Σ (B x) λ y → D x y z) ∘e
+    interchange-Σ-Σ ∘e
+    inv-associative-Σ' A B (λ x y → Σ (C x) (D x y))
+
   eq-interchange-Σ-Σ-is-contr :
     {a : A} {b : B a} → is-torsorial (D a b) →
     {x y : Σ (C a) (D a b)} →