Rename is-contr-total to is-torsorial (#871)

Since the definition of `is-torsorial` is that the total space is contractible, this pull request proposes to replace the clumsy-looking `is-contr-total` with `is-torsorial`.
UniMath · Oct 21, 2023 · fc26ae1 · fc26ae1
1 parent 94dd5a5
commit fc26ae1
Show file tree

Hide file tree

Showing 215 changed files with 1,217 additions and 1,217 deletions.
diff --git a/src/category-theory/full-large-subprecategories.lagda.md b/src/category-theory/full-large-subprecategories.lagda.md
@@ -208,8 +208,8 @@ module _
   is-large-category-large-precategory-is-large-category-Full-Large-Subprecategory
     is-large-category-C X =
     fundamental-theorem-id
-      ( is-contr-total-Eq-subtype
-        ( is-contr-total-iso-Large-Category
+      ( is-torsorial-Eq-subtype
+        ( is-torsorial-iso-Large-Category
           ( make-Large-Category C is-large-category-C)
           ( inclusion-subtype P X))
         ( is-prop-is-in-subtype P)

diff --git a/src/category-theory/full-subprecategories.lagda.md b/src/category-theory/full-subprecategories.lagda.md
@@ -245,8 +245,8 @@ module _
     is-category-Precategory (precategory-Full-Subprecategory C P)
   is-category-precategory-is-category-Full-Subprecategory is-category-C X =
     fundamental-theorem-id
-      ( is-contr-total-Eq-subtype
-        ( is-contr-total-iso-Category
+      ( is-torsorial-Eq-subtype
+        ( is-torsorial-iso-Category
           ( C , is-category-C)
           ( inclusion-subtype P X))
         ( is-prop-is-in-subtype P)

diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md
@@ -152,14 +152,14 @@ module _
               Σ ( Σ (pr1 yp ＝ x) (λ q → (q ∙ pr2 yp) ＝ refl))
                 ( λ ql → (pr2 yp ∙ pr1 ql) ＝ refl))))
         ( is-contr-Σ
-          ( is-contr-total-path x)
+          ( is-torsorial-path x)
           ( x , refl)
           ( is-contr-Σ
             ( is-contr-equiv
               ( Σ (x ＝ x) (λ q → q ＝ refl))
               ( equiv-tot
                 ( λ q → equiv-concat (inv right-unit) refl))
-              ( is-contr-total-path' refl))
+              ( is-torsorial-path' refl))
             ( refl , refl)
             ( is-proof-irrelevant-is-prop
               ( is-1-type-type-1-Type X x x refl refl)

diff --git a/src/category-theory/isomorphism-induction-categories.lagda.md b/src/category-theory/isomorphism-induction-categories.lagda.md
@@ -86,12 +86,12 @@ module _
   where
 
   abstract
-    is-identity-system-iso-is-contr-total-iso-Category :
+    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-contr-total-iso-Category =
-      is-identity-system-iso-is-contr-total-iso-Precategory
+    is-identity-system-iso-is-torsorial-iso-Category =
+      is-identity-system-iso-is-torsorial-iso-Precategory
         ( precategory-Category C)
 ```
 
@@ -102,12 +102,12 @@ module _
   {l1 l2 : Level} (C : Category l1 l2) {A : obj-Category C}
   where
 
-  is-contr-total-equiv-induction-principle-iso-Category :
+  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-contr-total-equiv-induction-principle-iso-Category =
-    is-contr-total-equiv-induction-principle-iso-Precategory
+  is-torsorial-equiv-induction-principle-iso-Category =
+    is-torsorial-equiv-induction-principle-iso-Precategory
       ( precategory-Category C)
 ```
 
@@ -122,8 +122,8 @@ module _
   abstract
     is-identity-system-iso-Category : section (ev-id-iso-Category C P)
     is-identity-system-iso-Category =
-      is-identity-system-iso-is-contr-total-iso-Category C
-        ( is-contr-total-iso-Category C A) P
+      is-identity-system-iso-is-torsorial-iso-Category C
+        ( is-torsorial-iso-Category C A) P
 
   ind-iso-Category :
     P A (id-iso-Category C) →
@@ -147,7 +147,7 @@ module _
   is-equiv-ev-id-iso-Category =
     dependent-universal-property-identity-system-is-torsorial
       ( id-iso-Category C)
-      ( is-contr-total-iso-Category C A)
+      ( is-torsorial-iso-Category C A)
       ( P)
 
   is-contr-map-ev-id-iso-Category :

diff --git a/src/category-theory/isomorphism-induction-precategories.lagda.md b/src/category-theory/isomorphism-induction-precategories.lagda.md
@@ -81,11 +81,11 @@ module _
   where
 
   abstract
-    is-identity-system-iso-is-contr-total-iso-Precategory :
+    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-contr-total-iso-Precategory =
+    is-identity-system-iso-is-torsorial-iso-Precategory =
       is-identity-system-is-torsorial A (id-iso-Precategory C)
 ```
 
@@ -96,10 +96,10 @@ module _
   {l1 l2 : Level} (C : Precategory l1 l2) {A : obj-Precategory C}
   where
 
-  is-contr-total-equiv-induction-principle-iso-Precategory :
+  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-contr-total-equiv-induction-principle-iso-Precategory =
+  is-torsorial-equiv-induction-principle-iso-Precategory =
     is-torsorial-is-identity-system A (id-iso-Precategory C)
 ```
diff --git a/src/category-theory/isomorphisms-in-categories.lagda.md b/src/category-theory/isomorphisms-in-categories.lagda.md
@@ -657,21 +657,21 @@ module _
   (X : obj-Category C)
   where
 
-  is-contr-total-iso-Category :
+  is-torsorial-iso-Category :
     is-contr (Σ (obj-Category C) (iso-Category C X))
-  is-contr-total-iso-Category =
+  is-torsorial-iso-Category =
     is-contr-equiv'
       ( Σ (obj-Category C) (X ＝_))
       ( equiv-tot (extensionality-obj-Category C X))
-      ( is-contr-total-path X)
+      ( is-torsorial-path X)
 
-  is-contr-total-iso-Category' :
+  is-torsorial-iso-Category' :
     is-contr (Σ (obj-Category C) (λ Y → iso-Category C Y X))
-  is-contr-total-iso-Category' =
+  is-torsorial-iso-Category' =
     is-contr-equiv'
       ( Σ (obj-Category C) (_＝ X))
       ( equiv-tot (λ Y → extensionality-obj-Category C Y X))
-      ( is-contr-total-path' X)
+      ( is-torsorial-path' X)
 ```
 
 ### Functoriality of `eq-iso`

diff --git a/src/category-theory/isomorphisms-in-large-categories.lagda.md b/src/category-theory/isomorphisms-in-large-categories.lagda.md
@@ -191,21 +191,21 @@ module _
   (X : obj-Large-Category C l1)
   where
 
-  is-contr-total-iso-Large-Category :
+  is-torsorial-iso-Large-Category :
     is-contr (Σ (obj-Large-Category C l1) (iso-Large-Category C X))
-  is-contr-total-iso-Large-Category =
+  is-torsorial-iso-Large-Category =
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (X ＝_))
       ( equiv-tot (extensionality-obj-Large-Category C X))
-      ( is-contr-total-path X)
+      ( is-torsorial-path X)
 
-  is-contr-total-iso-Large-Category' :
+  is-torsorial-iso-Large-Category' :
     is-contr (Σ (obj-Large-Category C l1) (λ Y → iso-Large-Category C Y X))
-  is-contr-total-iso-Large-Category' =
+  is-torsorial-iso-Large-Category' =
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (_＝ X))
       ( equiv-tot (λ Y → extensionality-obj-Large-Category C Y X))
-      ( is-contr-total-path' X)
+      ( is-torsorial-path' X)
 ```
 
 ## Properties

diff --git a/src/category-theory/maps-categories.lagda.md b/src/category-theory/maps-categories.lagda.md
@@ -96,11 +96,11 @@ module _
       ( precategory-Category C)
       ( precategory-Category D)
 
-  is-contr-total-htpy-map-Category :
+  is-torsorial-htpy-map-Category :
     (f : map-Category C D) →
     is-contr (Σ (map-Category C D) (htpy-map-Category f))
-  is-contr-total-htpy-map-Category =
-    is-contr-total-htpy-map-Precategory
+  is-torsorial-htpy-map-Category =
+    is-torsorial-htpy-map-Precategory
       ( precategory-Category C)
       ( precategory-Category D)
 

diff --git a/src/category-theory/maps-from-small-to-large-categories.lagda.md b/src/category-theory/maps-from-small-to-large-categories.lagda.md
@@ -89,13 +89,13 @@ module _
       ( precategory-Category C)
       ( large-precategory-Large-Category D)
 
-  is-contr-total-htpy-map-Small-Large-Category :
+  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-contr-total-htpy-map-Small-Large-Category =
-    is-contr-total-htpy-map-Small-Large-Precategory
+  is-torsorial-htpy-map-Small-Large-Category =
+    is-torsorial-htpy-map-Small-Large-Precategory
       ( precategory-Category C)
       ( large-precategory-Large-Category D)
 

diff --git a/src/category-theory/maps-from-small-to-large-precategories.lagda.md b/src/category-theory/maps-from-small-to-large-precategories.lagda.md
@@ -79,13 +79,13 @@ module _
   htpy-eq-map-Small-Large-Precategory =
     htpy-eq-map-Precategory C (precategory-Large-Precategory D γ)
 
-  is-contr-total-htpy-map-Small-Large-Precategory :
+  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-contr-total-htpy-map-Small-Large-Precategory =
-    is-contr-total-htpy-map-Precategory C (precategory-Large-Precategory D γ)
+  is-torsorial-htpy-map-Small-Large-Precategory =
+    is-torsorial-htpy-map-Precategory C (precategory-Large-Precategory D γ)
 
   is-equiv-htpy-eq-map-Small-Large-Precategory :
     (f g : map-Small-Large-Precategory C D γ) →

diff --git a/src/category-theory/maps-precategories.lagda.md b/src/category-theory/maps-precategories.lagda.md
@@ -161,16 +161,16 @@ module _
     (f g : map-Precategory C D) → (f ＝ g) → htpy-map-Precategory f g
   htpy-eq-map-Precategory f .f refl = refl-htpy-map-Precategory f
 
-  is-contr-total-htpy-map-Precategory :
+  is-torsorial-htpy-map-Precategory :
     (f : map-Precategory C D) →
     is-contr (Σ (map-Precategory C D) (htpy-map-Precategory f))
-  is-contr-total-htpy-map-Precategory f =
-    is-contr-total-Eq-structure _
-      ( is-contr-total-htpy (obj-map-Precategory C D f))
+  is-torsorial-htpy-map-Precategory f =
+    is-torsorial-Eq-structure _
+      ( is-torsorial-htpy (obj-map-Precategory C D f))
       ( obj-map-Precategory C D f , refl-htpy)
-      ( is-contr-total-Eq-implicit-Π _
+      ( is-torsorial-Eq-implicit-Π _
         ( λ x →
-          is-contr-total-Eq-implicit-Π _
+          is-torsorial-Eq-implicit-Π _
             ( λ y →
               is-contr-equiv
                 ( Σ
@@ -185,13 +185,13 @@ module _
                       ( inv-htpy (right-unit-law-comp-hom-Precategory D ∘ g₁))
                       ( left-unit-law-comp-hom-Precategory D ∘
                         hom-map-Precategory C D f)))
-                ( is-contr-total-htpy' (hom-map-Precategory C D f)))))
+                ( is-torsorial-htpy' (hom-map-Precategory C D f)))))
 
   is-equiv-htpy-eq-map-Precategory :
     (f g : map-Precategory C D) → is-equiv (htpy-eq-map-Precategory f g)
   is-equiv-htpy-eq-map-Precategory f =
     fundamental-theorem-id
-      ( is-contr-total-htpy-map-Precategory f)
+      ( is-torsorial-htpy-map-Precategory f)
       ( htpy-eq-map-Precategory f)
 
   equiv-htpy-eq-map-Precategory :

diff --git a/src/category-theory/slice-precategories.lagda.md b/src/category-theory/slice-precategories.lagda.md
@@ -197,7 +197,7 @@ module _
       ( Σ (hom-Precategory C A X) (λ g → f ＝ g))
       ( equiv-tot
         ( λ g → equiv-concat' f (left-unit-law-comp-hom-Precategory C g)))
-      ( is-contr-total-path f)
+      ( is-torsorial-path f)
 ```
 
 ### Products in slice precategories are pullbacks in the original category

diff --git a/src/commutative-algebra/homomorphisms-commutative-rings.lagda.md b/src/commutative-algebra/homomorphisms-commutative-rings.lagda.md
@@ -336,11 +336,11 @@ module _
       ( ring-Commutative-Ring B)
       ( f)
 
-  is-contr-total-htpy-hom-Commutative-Ring :
+  is-torsorial-htpy-hom-Commutative-Ring :
     is-contr
       ( Σ (hom-Commutative-Ring A B) (htpy-hom-Commutative-Ring A B f))
-  is-contr-total-htpy-hom-Commutative-Ring =
-    is-contr-total-htpy-hom-Ring
+  is-torsorial-htpy-hom-Commutative-Ring =
+    is-torsorial-htpy-hom-Ring
       ( ring-Commutative-Ring A)
       ( ring-Commutative-Ring B)
       ( f)

diff --git a/src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md b/src/commutative-algebra/homomorphisms-commutative-semirings.lagda.md
@@ -287,12 +287,12 @@ module _
   (f : hom-Commutative-Semiring A B)
   where
 
-  is-contr-total-htpy-hom-Commutative-Semiring :
+  is-torsorial-htpy-hom-Commutative-Semiring :
     is-contr
       ( Σ ( hom-Commutative-Semiring A B)
           ( htpy-hom-Commutative-Semiring A B f))
-  is-contr-total-htpy-hom-Commutative-Semiring =
-    is-contr-total-htpy-hom-Semiring
+  is-torsorial-htpy-hom-Commutative-Semiring =
+    is-torsorial-htpy-hom-Semiring
       ( semiring-Commutative-Semiring A)
       ( semiring-Commutative-Semiring B)
       ( f)

diff --git a/src/commutative-algebra/ideals-commutative-rings.lagda.md b/src/commutative-algebra/ideals-commutative-rings.lagda.md
@@ -237,12 +237,12 @@ module _
   refl-has-same-elements-ideal-Commutative-Ring =
     refl-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I
 
-  is-contr-total-has-same-elements-ideal-Commutative-Ring :
+  is-torsorial-has-same-elements-ideal-Commutative-Ring :
     is-contr
       ( Σ ( ideal-Commutative-Ring l2 R)
           ( has-same-elements-ideal-Commutative-Ring R I))
-  is-contr-total-has-same-elements-ideal-Commutative-Ring =
-    is-contr-total-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I
+  is-torsorial-has-same-elements-ideal-Commutative-Ring =
+    is-torsorial-has-same-elements-ideal-Ring (ring-Commutative-Ring R) I
 
   has-same-elements-eq-ideal-Commutative-Ring :
     (J : ideal-Commutative-Ring l2 R) →

diff --git a/src/commutative-algebra/isomorphisms-commutative-rings.lagda.md b/src/commutative-algebra/isomorphisms-commutative-rings.lagda.md
@@ -398,11 +398,11 @@ module _
   where
 
   abstract
-    is-contr-total-iso-Commutative-Ring :
+    is-torsorial-iso-Commutative-Ring :
       is-contr (Σ (Commutative-Ring l) (iso-Commutative-Ring A))
-    is-contr-total-iso-Commutative-Ring =
-      is-contr-total-Eq-subtype
-        ( is-contr-total-iso-Ring (ring-Commutative-Ring A))
+    is-torsorial-iso-Commutative-Ring =
+      is-torsorial-Eq-subtype
+        ( is-torsorial-iso-Ring (ring-Commutative-Ring A))
         ( is-prop-is-commutative-Ring)
         ( ring-Commutative-Ring A)
         ( id-iso-Ring (ring-Commutative-Ring A))
@@ -412,7 +412,7 @@ module _
     (B : Commutative-Ring l) → is-equiv (iso-eq-Commutative-Ring A B)
   is-equiv-iso-eq-Commutative-Ring =
     fundamental-theorem-id
-      ( is-contr-total-iso-Commutative-Ring)
+      ( is-torsorial-iso-Commutative-Ring)
       ( iso-eq-Commutative-Ring A)
 
   extensionality-Commutative-Ring :

diff --git a/src/commutative-algebra/radical-ideals-commutative-rings.lagda.md b/src/commutative-algebra/radical-ideals-commutative-rings.lagda.md
@@ -183,14 +183,14 @@ module _
     refl-has-same-elements-ideal-Commutative-Ring A
       ( ideal-radical-ideal-Commutative-Ring A I)
 
-  is-contr-total-has-same-elements-radical-ideal-Commutative-Ring :
+  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-contr-total-has-same-elements-radical-ideal-Commutative-Ring I =
-    is-contr-total-Eq-subtype
-      ( is-contr-total-has-same-elements-ideal-Commutative-Ring A
+  is-torsorial-has-same-elements-radical-ideal-Commutative-Ring I =
+    is-torsorial-Eq-subtype
+      ( is-torsorial-has-same-elements-ideal-Commutative-Ring A
         ( ideal-radical-ideal-Commutative-Ring A I))
       ( is-prop-is-radical-ideal-Commutative-Ring A)
       ( ideal-radical-ideal-Commutative-Ring A I)
@@ -208,7 +208,7 @@ module _
     is-equiv (has-same-elements-eq-radical-ideal-Commutative-Ring I J)
   is-equiv-has-same-elements-eq-radical-ideal-Commutative-Ring I =
     fundamental-theorem-id
-      ( is-contr-total-has-same-elements-radical-ideal-Commutative-Ring I)
+      ( is-torsorial-has-same-elements-radical-ideal-Commutative-Ring I)
       ( has-same-elements-eq-radical-ideal-Commutative-Ring I)
 
   extensionality-radical-ideal-Commutative-Ring :

diff --git a/src/elementary-number-theory/equality-integers.lagda.md b/src/elementary-number-theory/equality-integers.lagda.md
@@ -130,15 +130,15 @@ contraction-total-Eq-ℤ (inr (inr x)) (pair (inr (inr y)) e) =
     ( ap (inr ∘ inr) (eq-Eq-ℕ x y e))
     ( eq-is-prop (is-prop-Eq-ℕ x y))
 
-is-contr-total-Eq-ℤ :
+is-torsorial-Eq-ℤ :
   (x : ℤ) → is-contr (Σ ℤ (Eq-ℤ x))
-is-contr-total-Eq-ℤ x =
+is-torsorial-Eq-ℤ x =
   pair (pair x (refl-Eq-ℤ x)) (contraction-total-Eq-ℤ x)
 
 is-equiv-Eq-ℤ-eq :
   (x y : ℤ) → is-equiv (Eq-ℤ-eq {x} {y})
 is-equiv-Eq-ℤ-eq x =
   fundamental-theorem-id
-    ( is-contr-total-Eq-ℤ x)
+    ( is-torsorial-Eq-ℤ x)
     ( λ y → Eq-ℤ-eq {x} {y})
 ```