Equality in iterated Sigma types

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

@@ -106,13 +106,13 @@ module _
   η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
   η-pair t = eq-pair-Σ refl 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
+
+  inv-map-equiv-ap :
+    (e : A ≃ B) (x y : A) → (map-equiv e x ＝ map-equiv e y) → (x ＝ y)
+  inv-map-equiv-ap e x y = map-equiv (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,62 @@ module _
   triangle-eq-pair-Σ refl q = refl
 ```
 
+### Computing dependent identifications in iterated dependent pair types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3}
+  where
+
+  equiv-triple-eq-Σ :
+    (s t : Σ (Σ A B) C) →
+    (s ＝ t) ≃
+    ( Σ
+      ( Eq-Σ (pr1 s) (pr1 t))
+      ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 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-Σ (pr1 s) (pr1 t))
+      ( λ q → dependent-identification C (eq-pair-Σ' q) (pr2 s) (pr2 t)))
+  triple-eq-Σ s t = map-equiv (equiv-triple-eq-Σ s t)
+
+  coh-triple-Σ :
+    {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-triple-Σ refl = refl
+
+  dependent-eq-snd-eq-iterated-Σ :
+    (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-snd-eq-iterated-Σ s t p =
+    ( ap (λ q → tr B q (pr1 (pr2 s))) (coh-triple-Σ p)) ∙
+    ( pr2
+      ( pr1
+        ( map-equiv
+          ( equiv-triple-eq-Σ
+            ( map-inv-associative-Σ A B C s)
+            ( map-inv-associative-Σ A B C t))
+          ( ap (map-inv-associative-Σ A B C) 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-iterated-Σ-Σ :
+    Σ A (λ x → Σ (B x) (λ y → Σ (C x) (D x y))) ≃
+    Σ A (λ x → Σ (C x) (λ z → Σ (B x) λ y → D x y z))
+  interchange-iterated-Σ-Σ =
+    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)} →