Torsoriality of multivariable homotopies

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

@@ -51,7 +51,7 @@ of universe level `l₀ ⊔ l₁ ⊔ l₂ ⊔ l₃`.
 ```agda
 iterated-Σ : {l : Level} {n : ℕ} → telescope l n → UU l
 iterated-Σ (base-telescope A) = A
-iterated-Σ (cons-telescope A) = Σ _ (λ x → iterated-Σ (A x))
+iterated-Σ (cons-telescope {X = X} A) = Σ X (λ x → iterated-Σ (A x))
 ```
 
 ### Iterated elements of iterated type families
@@ -85,9 +85,8 @@ pr2 (iterated-pair (cons-iterated-element y a)) = iterated-pair a
 ```agda
 is-contr-Σ-telescope : {l : Level} {n : ℕ} → telescope l n → UU l
 is-contr-Σ-telescope (base-telescope A) = is-contr A
-is-contr-Σ-telescope (cons-telescope A) =
+is-contr-Σ-telescope (cons-telescope {X = X} A) =
   (is-contr X) × (Σ X (λ x → is-contr-Σ-telescope (A x)))
-  where X = _
 
 is-contr-iterated-Σ :
   {l : Level} (n : ℕ) {{A : telescope l n}} →
@@ -97,6 +96,22 @@ is-contr-iterated-Σ ._ {{cons-telescope A}} (is-contr-X , x , H) =
   is-contr-Σ is-contr-X x (is-contr-iterated-Σ _ {{A x}} H)
 ```
 
+### Contractiblity of iterated Σ-types without choice of contracting center
+
+```agda
+is-contr-Σ-telescope' : {l : Level} {n : ℕ} → telescope l n → UU l
+is-contr-Σ-telescope' (base-telescope A) = is-contr A
+is-contr-Σ-telescope' (cons-telescope {X = X} A) =
+  (is-contr X) × ((x : X) → is-contr-Σ-telescope' (A x))
+
+is-contr-iterated-Σ' :
+  {l : Level} (n : ℕ) {{A : telescope l n}} →
+  is-contr-Σ-telescope' A → is-contr (iterated-Σ A)
+is-contr-iterated-Σ' ._ {{base-telescope A}} is-contr-A = is-contr-A
+is-contr-iterated-Σ' ._ {{cons-telescope A}} (is-contr-X , H) =
+  is-contr-Σ' is-contr-X (λ x → is-contr-iterated-Σ' _ {{A x}} (H x))
+```
+
 ## See also
 
 - [Iterated Π-types](foundation.iterated-dependent-product-types.md)

src/foundation/subtype-identity-principle.lagda.md

@@ -49,16 +49,13 @@ module _
       is-torsorial B → ((x : A) → is-prop (P x)) →
       (a : A) (b : B a) (p : P a) →
       is-torsorial (λ (t : Σ A P) → B (pr1 t))
-    is-torsorial-Eq-subtype {l3} {P}
-      is-contr-AB is-subtype-P a b p =
+    is-torsorial-Eq-subtype {P = P} is-torsorial-B is-subtype-P a b p =
       is-contr-equiv
         ( Σ (Σ A B) (P ∘ pr1))
         ( equiv-right-swap-Σ)
         ( is-contr-equiv
           ( P a)
-          ( left-unit-law-Σ-is-contr
-            ( is-contr-AB)
-            ( pair a b))
+          ( left-unit-law-Σ-is-contr (is-torsorial-B) (a , b))
           ( is-proof-irrelevant-is-prop (is-subtype-P a) p))
 ```
 
@@ -76,7 +73,7 @@ module _
   abstract
     subtype-identity-principle :
       {f : (x : A) → a ＝ x → Eq-A x}
-      (h : (z : (Σ A P)) → (pair a p) ＝ z → Eq-A (pr1 z)) →
+      (h : (z : (Σ A P)) → (a , p) ＝ z → Eq-A (pr1 z)) →
       ((x : A) → is-equiv (f x)) → (z : Σ A P) → is-equiv (h z)
     subtype-identity-principle {f} h H =
       fundamental-theorem-id
@@ -95,12 +92,12 @@ module _
 
   map-extensionality-type-subtype :
     (f : (x : A) → (a ＝ x) ≃ Eq-A x) →
-    (z : Σ A (type-Prop ∘ P)) → (pair a p) ＝ z → Eq-A (pr1 z)
-  map-extensionality-type-subtype f .(pair a p) refl = refl-A
+    (z : Σ A (type-Prop ∘ P)) → (a , p) ＝ z → Eq-A (pr1 z)
+  map-extensionality-type-subtype f .(a , p) refl = refl-A
 
   extensionality-type-subtype :
     (f : (x : A) → (a ＝ x) ≃ Eq-A x) →
-    (z : Σ A (type-Prop ∘ P)) → (pair a p ＝ z) ≃ Eq-A (pr1 z)
+    (z : Σ A (type-Prop ∘ P)) → ((a , p) ＝ z) ≃ Eq-A (pr1 z)
   pr1 (extensionality-type-subtype f z) = map-extensionality-type-subtype f z
   pr2 (extensionality-type-subtype f z) =
     subtype-identity-principle

src/ring-theory/isomorphisms-rings.lagda.md

@@ -10,6 +10,7 @@ module ring-theory.isomorphisms-rings where
 open import category-theory.isomorphisms-in-large-precategories
 
 open import foundation.action-on-identifications-functions
+open import foundation.binary-homotopies
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equality-dependent-function-types
@@ -485,15 +486,9 @@ module _
             ( is-torsorial-Eq-subtype
               ( is-contr-equiv
                 ( Σ ( (x y : type-Ring R) → type-Ring R)
-                    ( λ g →
-                      (x y : type-Ring R) → mul-Ring R x y ＝ g x y))
-                ( equiv-tot
-                  ( λ m →
-                    equiv-Π-equiv-family (λ x → equiv-explicit-implicit-Π) ∘e
-                    equiv-explicit-implicit-Π))
-                ( is-torsorial-Eq-Π
-                  ( λ x m → (y : type-Ring R) → mul-Ring R x y ＝ m y)
-                  ( λ x → is-torsorial-htpy (mul-Ring R x))))
+                    ( λ g → (x y : type-Ring R) → mul-Ring R x y ＝ g x y))
+                ( equiv-tot (λ _ → equiv-explicit-implicit-iterated-Π 2))
+                ( is-torsorial-binary-htpy (mul-Ring R)))
               ( λ μ →
                 is-prop-iterated-Π 3
                   ( λ x y z → is-set-type-Ring R (μ (μ x y) z) (μ x (μ y z))))