Implement is-torsorial throughout the library

src/category-theory/isomorphism-induction-categories.lagda.md

@@ -20,6 +20,7 @@ open import foundation.function-types
 open import foundation.identity-systems
 open import foundation.identity-types
 open import foundation.sections
+open import foundation.torsorial-type-families
 open import foundation.universal-property-identity-systems
 open import foundation.universe-levels
 ```
@@ -78,39 +79,6 @@ module _
 
 ## Properties
 
-### Contractibility of the total space of isomorphisms implies isomorphism induction
-
-```agda
-module _
-  {l1 l2 : Level} (C : Category l1 l2) {A : obj-Category C}
-  where
-
-  abstract
-    is-identity-system-iso-is-torsorial-iso-Category :
-      is-contr (Σ (obj-Category C) (iso-Category C A)) →
-      {l : Level} →
-      is-identity-system l (iso-Category C A) A (id-iso-Category C)
-    is-identity-system-iso-is-torsorial-iso-Category =
-      is-identity-system-iso-is-torsorial-iso-Precategory
-        ( precategory-Category C)
-```
-
-### Isomorphism induction implies contractibility of the total space of isomorphisms
-
-```agda
-module _
-  {l1 l2 : Level} (C : Category l1 l2) {A : obj-Category C}
-  where
-
-  is-torsorial-equiv-induction-principle-iso-Category :
-    ( {l : Level} →
-      is-identity-system l (iso-Category C A) A (id-iso-Category C)) →
-    is-contr (Σ (obj-Category C) (iso-Category C A))
-  is-torsorial-equiv-induction-principle-iso-Category =
-    is-torsorial-equiv-induction-principle-iso-Precategory
-      ( precategory-Category C)
-```
-
 ### Isomorphism induction in a category
 
 ```agda
@@ -122,8 +90,10 @@ module _
   abstract
     is-identity-system-iso-Category : section (ev-id-iso-Category C P)
     is-identity-system-iso-Category =
-      is-identity-system-iso-is-torsorial-iso-Category C
-        ( is-torsorial-iso-Category C A) P
+      is-identity-system-is-torsorial-iso-Precategory
+        ( precategory-Category C)
+        ( is-torsorial-iso-Category C A)
+        ( P)
 
   ind-iso-Category :
     P A (id-iso-Category C) →

src/category-theory/isomorphism-induction-precategories.lagda.md

@@ -17,6 +17,7 @@ open import foundation.function-types
 open import foundation.identity-systems
 open import foundation.identity-types
 open import foundation.sections
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -81,11 +82,10 @@ module _
   where
 
   abstract
-    is-identity-system-iso-is-torsorial-iso-Precategory :
-      is-contr (Σ (obj-Precategory C) (iso-Precategory C A)) →
-      {l : Level} →
-      is-identity-system l (iso-Precategory C A) A (id-iso-Precategory C)
-    is-identity-system-iso-is-torsorial-iso-Precategory =
+    is-identity-system-is-torsorial-iso-Precategory :
+      is-torsorial (iso-Precategory C A) →
+      is-identity-system (iso-Precategory C A) A (id-iso-Precategory C)
+    is-identity-system-is-torsorial-iso-Precategory =
       is-identity-system-is-torsorial A (id-iso-Precategory C)
 ```
 
@@ -97,9 +97,8 @@ module _
   where
 
   is-torsorial-equiv-induction-principle-iso-Precategory :
-    ( {l : Level} →
-      is-identity-system l (iso-Precategory C A) A (id-iso-Precategory C)) →
-    is-contr (Σ (obj-Precategory C) (iso-Precategory C A))
+    is-identity-system (iso-Precategory C A) A (id-iso-Precategory C) →
+    is-torsorial (iso-Precategory C A)
   is-torsorial-equiv-induction-principle-iso-Precategory =
     is-torsorial-is-identity-system A (id-iso-Precategory C)
 ```

src/category-theory/isomorphisms-in-categories.lagda.md

@@ -19,6 +19,7 @@ open import foundation.functoriality-dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -658,15 +659,15 @@ module _
   where
 
   is-torsorial-iso-Category :
-    is-contr (Σ (obj-Category C) (iso-Category C X))
+    is-torsorial (iso-Category C X)
   is-torsorial-iso-Category =
     is-contr-equiv'
       ( Σ (obj-Category C) (X ＝_))
       ( equiv-tot (extensionality-obj-Category C X))
       ( is-torsorial-path X)
 
   is-torsorial-iso-Category' :
-    is-contr (Σ (obj-Category C) (λ Y → iso-Category C Y X))
+    is-torsorial (λ Y → iso-Category C Y X)
   is-torsorial-iso-Category' =
     is-contr-equiv'
       ( Σ (obj-Category C) (_＝ X))

src/category-theory/isomorphisms-in-large-categories.lagda.md

@@ -19,6 +19,7 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -193,15 +194,15 @@ module _
   where
 
   is-torsorial-iso-Large-Category :
-    is-contr (Σ (obj-Large-Category C l1) (iso-Large-Category C X))
+    is-torsorial (iso-Large-Category C X)
   is-torsorial-iso-Large-Category =
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (X ＝_))
       ( equiv-tot (extensionality-obj-Large-Category C X))
       ( is-torsorial-path X)
 
   is-torsorial-iso-Large-Category' :
-    is-contr (Σ (obj-Large-Category C l1) (λ Y → iso-Large-Category C Y X))
+    is-torsorial (λ Y → iso-Large-Category C Y X)
   is-torsorial-iso-Large-Category' =
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (_＝ X))

src/category-theory/maps-categories.lagda.md

@@ -15,6 +15,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -97,8 +98,7 @@ module _
       ( precategory-Category D)
 
   is-torsorial-htpy-map-Category :
-    (f : map-Category C D) →
-    is-contr (Σ (map-Category C D) (htpy-map-Category f))
+    (f : map-Category C D) → is-torsorial (htpy-map-Category f)
   is-torsorial-htpy-map-Category =
     is-torsorial-htpy-map-Precategory
       ( precategory-Category C)

src/category-theory/maps-from-small-to-large-categories.lagda.md

@@ -15,6 +15,7 @@ open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -91,9 +92,7 @@ module _
 
   is-torsorial-htpy-map-Small-Large-Category :
     (f : map-Small-Large-Category C D γ) →
-    is-contr
-      ( Σ ( map-Small-Large-Category C D γ)
-          ( htpy-map-Small-Large-Category f))
+    is-torsorial (htpy-map-Small-Large-Category f)
   is-torsorial-htpy-map-Small-Large-Category =
     is-torsorial-htpy-map-Small-Large-Precategory
       ( precategory-Category C)

src/category-theory/maps-from-small-to-large-precategories.lagda.md

@@ -15,6 +15,7 @@ open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -81,9 +82,7 @@ module _
 
   is-torsorial-htpy-map-Small-Large-Precategory :
     (f : map-Small-Large-Precategory C D γ) →
-    is-contr
-      ( Σ ( map-Small-Large-Precategory C D γ)
-          ( htpy-map-Small-Large-Precategory f))
+    is-torsorial (htpy-map-Small-Large-Precategory f)
   is-torsorial-htpy-map-Small-Large-Precategory =
     is-torsorial-htpy-map-Precategory C (precategory-Large-Precategory D γ)
 

src/category-theory/maps-precategories.lagda.md

@@ -22,6 +22,7 @@ open import foundation.homotopies
 open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -162,8 +163,7 @@ module _
   htpy-eq-map-Precategory f .f refl = refl-htpy-map-Precategory f
 
   is-torsorial-htpy-map-Precategory :
-    (f : map-Precategory C D) →
-    is-contr (Σ (map-Precategory C D) (htpy-map-Precategory f))
+    (f : map-Precategory C D) → is-torsorial (htpy-map-Precategory f)
   is-torsorial-htpy-map-Precategory f =
     is-torsorial-Eq-structure _
       ( is-torsorial-htpy (obj-map-Precategory C D f))

src/commutative-algebra/homomorphisms-commutative-rings.lagda.md

@@ -17,6 +17,7 @@ open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.sets
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 
 open import group-theory.homomorphisms-abelian-groups
@@ -337,8 +338,7 @@ module _
       ( f)
 
   is-torsorial-htpy-hom-Commutative-Ring :
-    is-contr
-      ( Σ (hom-Commutative-Ring A B) (htpy-hom-Commutative-Ring A B f))
+    is-torsorial (htpy-hom-Commutative-Ring A B f)
   is-torsorial-htpy-hom-Commutative-Ring =
     is-torsorial-htpy-hom-Ring
       ( ring-Commutative-Ring A)

src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md

@@ -14,6 +14,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.sets
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 
 open import group-theory.homomorphisms-commutative-monoids
@@ -288,9 +289,7 @@ module _
   where
 
   is-torsorial-htpy-hom-Commutative-Semiring :
-    is-contr
-      ( Σ ( hom-Commutative-Semiring A B)
-          ( htpy-hom-Commutative-Semiring A B f))
+    is-torsorial (htpy-hom-Commutative-Semiring A B f)
   is-torsorial-htpy-hom-Commutative-Semiring =
     is-torsorial-htpy-hom-Semiring
       ( semiring-Commutative-Semiring A)

src/commutative-algebra/ideals-commutative-rings.lagda.md

@@ -18,6 +18,7 @@ open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
 open import foundation.propositions
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 
 open import ring-theory.ideals-rings
@@ -238,9 +239,7 @@ module _
     refl-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I
 
   is-torsorial-has-same-elements-ideal-Commutative-Ring :
-    is-contr
-      ( Σ ( ideal-Commutative-Ring l2 R)
-          ( has-same-elements-ideal-Commutative-Ring R I))
+    is-torsorial (has-same-elements-ideal-Commutative-Ring R I)
   is-torsorial-has-same-elements-ideal-Commutative-Ring =
     is-torsorial-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I
 

src/commutative-algebra/isomorphisms-commutative-rings.lagda.md

@@ -23,6 +23,7 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtype-identity-principle
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 
 open import group-theory.isomorphisms-abelian-groups
@@ -399,7 +400,7 @@ module _
 
   abstract
     is-torsorial-iso-Commutative-Ring :
-      is-contr (Σ (Commutative-Ring l) (iso-Commutative-Ring A))
+      is-torsorial (λ (B : Commutative-Ring l) → iso-Commutative-Ring A B)
     is-torsorial-iso-Commutative-Ring =
       is-torsorial-Eq-subtype
         ( is-torsorial-iso-Ring (ring-Commutative-Ring A))

src/commutative-algebra/radical-ideals-commutative-rings.lagda.md

@@ -21,6 +21,7 @@ open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtype-identity-principle
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -185,9 +186,8 @@ module _
 
   is-torsorial-has-same-elements-radical-ideal-Commutative-Ring :
     {l2 : Level} (I : radical-ideal-Commutative-Ring l2 A) →
-    is-contr
-      ( Σ ( radical-ideal-Commutative-Ring l2 A)
-          ( has-same-elements-radical-ideal-Commutative-Ring I))
+    is-torsorial
+      ( has-same-elements-radical-ideal-Commutative-Ring I)
   is-torsorial-has-same-elements-radical-ideal-Commutative-Ring I =
     is-torsorial-Eq-subtype
       ( is-torsorial-has-same-elements-ideal-Commutative-Ring A

src/elementary-number-theory/equality-integers.lagda.md

@@ -26,6 +26,7 @@ open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.set-truncations
+open import foundation.torsorial-type-families
 open import foundation.unit-type
 open import foundation.universe-levels
 ```
@@ -131,7 +132,7 @@ contraction-total-Eq-ℤ (inr (inr x)) (pair (inr (inr y)) e) =
     ( eq-is-prop (is-prop-Eq-ℕ x y))
 
 is-torsorial-Eq-ℤ :
-  (x : ℤ) → is-contr (Σ ℤ (Eq-ℤ x))
+  (x : ℤ) → is-torsorial (Eq-ℤ x)
 is-torsorial-Eq-ℤ x =
   pair (pair x (refl-Eq-ℤ x)) (contraction-total-Eq-ℤ x)
 

src/elementary-number-theory/equality-natural-numbers.lagda.md

@@ -24,6 +24,7 @@ open import foundation.unit-type
 open import foundation.universe-levels
 
 open import foundation-core.decidable-propositions
+open import foundation-core.torsorial-type-families
 ```
 
 </details>
@@ -80,7 +81,7 @@ pr1 (map-total-Eq-ℕ m (pair n e)) = succ-ℕ n
 pr2 (map-total-Eq-ℕ m (pair n e)) = e
 
 is-torsorial-Eq-ℕ :
-  (m : ℕ) → is-contr (Σ ℕ (Eq-ℕ m))
+  (m : ℕ) → is-torsorial (Eq-ℕ m)
 pr1 (pr1 (is-torsorial-Eq-ℕ m)) = m
 pr2 (pr1 (is-torsorial-Eq-ℕ m)) = refl-Eq-ℕ m
 pr2 (is-torsorial-Eq-ℕ zero-ℕ) (pair zero-ℕ star) = refl

src/elementary-number-theory/prime-numbers.lagda.md

@@ -29,6 +29,7 @@ open import foundation.logical-equivalences
 open import foundation.negated-equality
 open import foundation.negation
 open import foundation.propositions
+open import foundation.torsorial-type-families
 open import foundation.transport-along-identifications
 open import foundation.unit-type
 open import foundation.universe-levels
@@ -82,7 +83,7 @@ is-prime-easy-ℕ n = (is-not-one-ℕ n) × (is-one-is-proper-divisor-ℕ n)
 
 ```agda
 has-unique-proper-divisor-ℕ : ℕ → UU lzero
-has-unique-proper-divisor-ℕ n = is-contr (Σ ℕ (is-proper-divisor-ℕ n))
+has-unique-proper-divisor-ℕ n = is-torsorial (is-proper-divisor-ℕ n)
 ```
 
 ## Properties

src/elementary-number-theory/universal-property-integers.lagda.md

@@ -23,6 +23,7 @@ open import foundation.homotopy-induction
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.structure-identity-principle
+open import foundation.torsorial-type-families
 open import foundation.universe-levels
 ```
 
@@ -149,7 +150,7 @@ abstract
   is-torsorial-Eq-ELIM-ℤ :
     { l1 : Level} (P : ℤ → UU l1) →
     ( p0 : P zero-ℤ) (pS : (k : ℤ) → (P k) ≃ (P (succ-ℤ k))) →
-    ( s : ELIM-ℤ P p0 pS) → is-contr (Σ (ELIM-ℤ P p0 pS) (Eq-ELIM-ℤ P p0 pS s))
+    ( s : ELIM-ℤ P p0 pS) → is-torsorial (Eq-ELIM-ℤ P p0 pS s)
   is-torsorial-Eq-ELIM-ℤ P p0 pS s =
     is-torsorial-Eq-structure
       ( λ f t H →