Rename is-torsorial-path to is-torsorial-Id (#1016)

That's it. Also renames `is-torsorial-path'` to `is-torsorial-Id'`.

src/category-theory/groupoids.lagda.md

@@ -165,12 +165,12 @@ module _
               Σ ( Σ (y ＝ x) (λ q → q ∙ p ＝ refl))
                 ( λ (q , l) → p ∙ q ＝ refl))))
         ( is-contr-iterated-Σ 2
-          ( is-torsorial-path x ,
+          ( is-torsorial-Id x ,
             ( x , refl) ,
             ( is-contr-equiv
               ( Σ (x ＝ x) (λ q → q ＝ refl))
               ( equiv-tot (λ q → equiv-concat (inv right-unit) refl))
-              ( is-torsorial-path' refl)) ,
+              ( is-torsorial-Id' refl)) ,
             ( refl , refl) ,
             ( is-proof-irrelevant-is-prop
               ( is-1-type-type-1-Type X x x refl refl)

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

@@ -743,15 +743,15 @@ module _
     is-contr-equiv'
       ( Σ (obj-Category C) (X ＝_))
       ( equiv-tot (extensionality-obj-Category C X))
-      ( is-torsorial-path X)
+      ( is-torsorial-Id X)
 
   is-torsorial-iso-Category' :
     is-torsorial (λ Y → iso-Category C Y X)
   is-torsorial-iso-Category' =
     is-contr-equiv'
       ( Σ (obj-Category C) (_＝ X))
       ( equiv-tot (λ Y → extensionality-obj-Category C Y X))
-      ( is-torsorial-path' X)
+      ( is-torsorial-Id' X)
 ```
 
 ### Functoriality of `eq-iso`

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

@@ -199,15 +199,15 @@ module _
     is-contr-equiv'
       ( Σ (obj-Large-Category C l1) (X ＝_))
       ( equiv-tot (extensionality-obj-Large-Category C X))
-      ( is-torsorial-path X)
+      ( is-torsorial-Id X)
 
   is-torsorial-iso-Large-Category' :
     is-torsorial (λ Y → iso-Large-Category C Y X)
   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-torsorial-path' X)
+      ( is-torsorial-Id' X)
 ```
 
 ## Properties

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

@@ -212,7 +212,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-torsorial-path f)
+      ( is-torsorial-Id f)
 ```
 
 ### Products in slice precategories are pullbacks in the original category

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

@@ -161,7 +161,7 @@ abstract
           ( tot (λ α → right-transpose-eq-concat refl α (pr1 (pr2 s))))
           ( is-equiv-tot-is-fiberwise-equiv
             ( λ α → is-equiv-right-transpose-eq-concat refl α (pr1 (pr2 s))))
-          ( is-torsorial-path' (pr1 (pr2 s))))
+          ( is-torsorial-Id' (pr1 (pr2 s))))
         ( pair (pr1 (pr2 s)) (inv (right-inv (pr1 (pr2 s)))))
         ( is-contr-is-equiv'
           ( Σ ( ( k : ℤ) → Id (pr1 s (succ-ℤ k)) (pr1 (pS k) (pr1 s k)))

src/elementary-number-theory/universal-property-natural-numbers.lagda.md

@@ -69,7 +69,7 @@ module _
       ( is-torsorial-htpy (pr1 h))
       ( pair (pr1 h) refl-htpy)
       ( is-torsorial-Eq-structure
-        ( is-torsorial-path (pr1 (pr2 h)))
+        ( is-torsorial-Id (pr1 (pr2 h)))
         ( pair (pr1 (pr2 h)) refl)
         ( is-torsorial-htpy (λ n → (pr2 (pr2 h) n ∙ refl))))
 

src/foundation-core/contractible-types.lagda.md

@@ -82,16 +82,16 @@ module _
   where
 
   abstract
-    is-torsorial-path : (a : A) → is-contr (Σ A (λ x → a ＝ x))
-    pr1 (pr1 (is-torsorial-path a)) = a
-    pr2 (pr1 (is-torsorial-path a)) = refl
-    pr2 (is-torsorial-path a) (pair .a refl) = refl
+    is-torsorial-Id : (a : A) → is-contr (Σ A (λ x → a ＝ x))
+    pr1 (pr1 (is-torsorial-Id a)) = a
+    pr2 (pr1 (is-torsorial-Id a)) = refl
+    pr2 (is-torsorial-Id a) (pair .a refl) = refl
 
   abstract
-    is-torsorial-path' : (a : A) → is-contr (Σ A (λ x → x ＝ a))
-    pr1 (pr1 (is-torsorial-path' a)) = a
-    pr2 (pr1 (is-torsorial-path' a)) = refl
-    pr2 (is-torsorial-path' a) (pair .a refl) = refl
+    is-torsorial-Id' : (a : A) → is-contr (Σ A (λ x → x ＝ a))
+    pr1 (pr1 (is-torsorial-Id' a)) = a
+    pr2 (pr1 (is-torsorial-Id' a)) = refl
+    pr2 (is-torsorial-Id' a) (pair .a refl) = refl
 ```
 
 ## Properties

src/foundation/embeddings.lagda.md

@@ -279,7 +279,7 @@ module _
   is-section-inv-map-Σ-emb-base (b , c) =
     ap
       ( λ s → (pr1 s , inv-tr C (pr2 s) c))
-      ( eq-is-contr (is-torsorial-path' b))
+      ( eq-is-contr (is-torsorial-Id' b))
 
   is-retraction-inv-map-Σ-emb-base :
     is-retraction (map-Σ-map-base (map-emb f) C) inv-map-Σ-emb-base

src/foundation/equality-coproduct-types.lagda.md

@@ -230,7 +230,7 @@ module _
         ( is-contr-equiv
           ( Σ A (Id x))
           ( equiv-tot (compute-eq-coprod-inl-inl x))
-          ( is-torsorial-path x))
+          ( is-torsorial-Id x))
         ( λ y → ap inl)
 
   emb-inl : A ↪ (A + B)
@@ -244,7 +244,7 @@ module _
         ( is-contr-equiv
           ( Σ B (Id x))
           ( equiv-tot (compute-eq-coprod-inr-inr x))
-          ( is-torsorial-path x))
+          ( is-torsorial-Id x))
         ( λ y → ap inr)
 
   emb-inr : B ↪ (A + B)

src/foundation/families-of-maps.lagda.md

@@ -56,7 +56,7 @@ module _
       ≃ (((x , _) : Σ A B) →
           Σ (Σ A (x ＝_)) λ (x' , _) → C x') by equiv-Π-equiv-family (λ (x , _) →
                                                   inv-left-unit-law-Σ-is-contr
-                                                    (is-torsorial-path x)
+                                                    (is-torsorial-Id x)
                                                     (x , refl))
       ≃ (((x , _) : Σ A B) →
           Σ (Σ A C) λ (x' , _) → x ＝ x') by equiv-Π-equiv-family (λ (x , _) →

src/foundation/functional-correspondences.lagda.md

@@ -155,7 +155,7 @@ module _
     ((x : A) → B x) → functional-correspondence l2 A B
   pr1 (functional-correspondence-function f) x y = f x ＝ y
   pr2 (functional-correspondence-function f) x =
-    is-torsorial-path (f x)
+    is-torsorial-Id (f x)
 
   function-functional-correspondence :
     {l3 : Level} → functional-correspondence l3 A B → ((x : A) → B x)

src/foundation/fundamental-theorem-of-identity-types.lagda.md

@@ -61,7 +61,7 @@ module _
       is-torsorial B → (f : (x : A) → a ＝ x → B x) → is-fiberwise-equiv f
     fundamental-theorem-id is-contr-AB f =
       is-fiberwise-equiv-is-equiv-tot
-        ( is-equiv-is-contr (tot f) (is-torsorial-path a) is-contr-AB)
+        ( is-equiv-is-contr (tot f) (is-torsorial-Id a) is-contr-AB)
 
   abstract
     fundamental-theorem-id' :
@@ -71,7 +71,7 @@ module _
         ( Σ A (Id a))
         ( tot f)
         ( is-equiv-tot-is-fiberwise-equiv is-fiberwise-equiv-f)
-        ( is-torsorial-path a)
+        ( is-torsorial-Id a)
 ```
 
 ## Corollaries
@@ -95,7 +95,7 @@ module _
         ( Σ A (Id a))
         ( tot (ind-Id a (λ x p → B x) b))
         ( is-equiv-tot-is-fiberwise-equiv H)
-        ( is-torsorial-path a)
+        ( is-torsorial-Id a)
 ```
 
 ### Retracts of the identity type are equivalent to the identity type
@@ -120,8 +120,8 @@ module _
               ( ( inv-htpy (preserves-comp-tot i (pr1 ∘ R))) ∙h
                 ( tot-htpy (pr2 ∘ R)) ∙h
                 ( tot-id B)))
-            ( is-torsorial-path a))
-          ( is-torsorial-path a))
+            ( is-torsorial-Id a))
+          ( is-torsorial-Id a))
 
     fundamental-theorem-id-retract :
       (R : (x : A) → (B x) retract-of (a ＝ x)) →

src/foundation/homotopy-induction.lagda.md

@@ -90,15 +90,15 @@ module _
       is-contr-equiv'
         ( Σ ((x : A) → B x) (Id f))
         ( equiv-tot (λ g → equiv-funext))
-        ( is-torsorial-path f)
+        ( is-torsorial-Id f)
 
   abstract
     is-torsorial-htpy' : is-torsorial (λ g → g ~ f)
     is-torsorial-htpy' =
       is-contr-equiv'
         ( Σ ((x : A) → B x) (λ g → g ＝ f))
         ( equiv-tot (λ g → equiv-funext))
-        ( is-torsorial-path' f)
+        ( is-torsorial-Id' f)
 ```
 
 ### Homotopy induction is equivalent to function extensionality

src/foundation/images.lagda.md

@@ -94,7 +94,7 @@ module _
       (x : im f) → is-torsorial (Eq-im x)
     is-torsorial-Eq-im x =
       is-torsorial-Eq-subtype
-        ( is-torsorial-path (pr1 x))
+        ( is-torsorial-Id (pr1 x))
         ( λ x → is-prop-type-trunc-Prop)
         ( pr1 x)
         ( refl)

src/foundation/logical-equivalences.lagda.md

@@ -165,7 +165,7 @@ compute-fiber-iff-equiv :
   fiber (iff-equiv) (f , g) ≃ Σ (is-equiv f) (λ f' → map-inv-is-equiv f' ~ g)
 compute-fiber-iff-equiv {A = A} {B} (f , g) =
   ( equiv-tot (λ _ → equiv-funext)) ∘e
-  ( left-unit-law-Σ-is-contr (is-torsorial-path' f) (f , refl)) ∘e
+  ( left-unit-law-Σ-is-contr (is-torsorial-Id' f) (f , refl)) ∘e
   ( inv-associative-Σ (A → B) (_＝ f) _) ∘e
   ( equiv-tot (λ _ → equiv-left-swap-Σ)) ∘e
   ( associative-Σ (A → B) _ _) ∘e

src/foundation/multivariable-homotopies.lagda.md

@@ -194,7 +194,7 @@ abstract
   is-torsorial-multivariable-htpy :
     {l : Level} (n : ℕ) {{A : telescope l n}} (f : iterated-Π A) →
     is-torsorial (multivariable-htpy {{A}} f)
-  is-torsorial-multivariable-htpy .0 {{base-telescope A}} = is-torsorial-path
+  is-torsorial-multivariable-htpy .0 {{base-telescope A}} = is-torsorial-Id
   is-torsorial-multivariable-htpy ._ {{cons-telescope A}} f =
     is-torsorial-Eq-Π (λ x → is-torsorial-multivariable-htpy _ {{A x}} (f x))
 
@@ -206,7 +206,7 @@ abstract
     is-contr-equiv'
       ( Σ (iterated-implicit-Π A) (Id {A = iterated-implicit-Π A} f))
       ( equiv-tot (λ _ → equiv-iterated-funext-implicit _ {{A}}))
-      ( is-torsorial-path {A = iterated-implicit-Π A} f)
+      ( is-torsorial-Id {A = iterated-implicit-Π A} f)
 
 abstract
   is-torsorial-multivariable-implicit-htpy :

src/foundation/pairs-of-distinct-elements.lagda.md

@@ -84,10 +84,10 @@ module _
     is-torsorial (Eq-pair-of-distinct-elements p)
   is-torsorial-Eq-pair-of-distinct-elements p =
     is-torsorial-Eq-structure
-      ( is-torsorial-path (first-pair-of-distinct-elements p))
+      ( is-torsorial-Id (first-pair-of-distinct-elements p))
       ( pair (first-pair-of-distinct-elements p) refl)
       ( is-torsorial-Eq-subtype
-        ( is-torsorial-path (second-pair-of-distinct-elements p))
+        ( is-torsorial-Id (second-pair-of-distinct-elements p))
         ( λ x → is-prop-neg)
         ( second-pair-of-distinct-elements p)
         ( refl)

src/foundation/partitions.lagda.md

@@ -641,7 +641,7 @@ module _
                         ( subtype-inhabited-subtype Q x)) ∘e
                     ( equiv-inv-equiv))) ∘e
                 ( left-unit-law-Σ-is-contr
-                  ( is-torsorial-path (index-Set-Indexed-Σ-Decomposition D a))
+                  ( is-torsorial-Id (index-Set-Indexed-Σ-Decomposition D a))
                   ( pair
                     ( index-Set-Indexed-Σ-Decomposition D a)
                     ( refl)))) ∘e

src/foundation/pullbacks.lagda.md

@@ -1145,11 +1145,11 @@ module _
             ( c)
             ( cone-ap' c1))
           ( is-equiv-is-contr _
-            ( is-torsorial-path (horizontal-map-cone f g c c1))
-            ( is-torsorial-path (f (vertical-map-cone f g c c1))))
+            ( is-torsorial-Id (horizontal-map-cone f g c c1))
+            ( is-torsorial-Id (f (vertical-map-cone f g c c1))))
           ( is-equiv-is-contr _
-            ( is-torsorial-path c1)
-            ( is-torsorial-path (vertical-map-cone f g c c1))))
+            ( is-torsorial-Id c1)
+            ( is-torsorial-Id (vertical-map-cone f g c c1))))
         ( c2))
 ```
 

src/foundation/russells-paradox.lagda.md

@@ -129,7 +129,7 @@ paradox-Russell {l} H =
     β = ( equiv-precomp α empty) ∘e
         ( ( left-unit-law-Σ-is-contr
             { B = λ t → (pr1 t) ∉-𝕍 (pr1 t)}
-            ( is-torsorial-path' R')
+            ( is-torsorial-Id' R')
             ( pair R' refl)) ∘e
           ( ( inv-associative-Σ (𝕍 l) (_＝ R') (λ t → (pr1 t) ∉-𝕍 (pr1 t))) ∘e
             ( ( equiv-tot

src/foundation/sections.lagda.md

@@ -139,7 +139,7 @@ module _
       ( is-contr-equiv
         ( Π-total-fam (λ x y → y ＝ x))
         ( inv-distributive-Π-Σ)
-        ( is-contr-Π is-torsorial-path'))
+        ( is-contr-Π is-torsorial-Id'))
       ( id , refl-htpy)) ∘e
     ( equiv-right-swap-Σ) ∘e
     ( equiv-Σ-equiv-base ( λ s → pr1 s ~ id) ( distributive-Π-Σ))

src/foundation/sequential-limits.lagda.md

@@ -193,7 +193,7 @@ module _
     is-torsorial-Eq-structure
       ( is-torsorial-htpy (pr1 s))
       ( pr1 s , refl-htpy)
-      ( is-torsorial-Eq-Π (λ n → is-torsorial-path (pr2 s n ∙ refl)))
+      ( is-torsorial-Eq-Π (λ n → is-torsorial-Id (pr2 s n ∙ refl)))
 
   is-equiv-Eq-eq-standard-sequential-limit :
     (s t : standard-sequential-limit A) →

src/foundation/singleton-subtypes.lagda.md

@@ -105,7 +105,7 @@ module _
 
   standard-singleton-subtype : singleton-subtype l (type-Set X)
   pr1 standard-singleton-subtype = subtype-standard-singleton-subtype
-  pr2 standard-singleton-subtype = is-torsorial-path x
+  pr2 standard-singleton-subtype = is-torsorial-Id x
 
   inhabited-subtype-standard-singleton-subtype :
     inhabited-subtype l (type-Set X)
@@ -248,8 +248,8 @@ module _
             ( λ y →
               ( inv-equiv (equiv-unit-trunc-Prop (Id-Prop Y (f x) y))) ∘e
               ( equiv-trunc-Prop
-                ( left-unit-law-Σ-is-contr (is-torsorial-path x) (x , refl)))))
-        ( is-torsorial-path (f x))
+                ( left-unit-law-Σ-is-contr (is-torsorial-Id x) (x , refl)))))
+        ( is-torsorial-Id (f x))
 
   compute-im-singleton-subtype :
     has-same-elements-subtype
@@ -261,7 +261,7 @@ module _
       ( im-subtype f (subtype-standard-singleton-subtype X x))
       ( refl)
       ( unit-trunc-Prop ((x , refl) , refl))
-      ( is-torsorial-path (f x))
+      ( is-torsorial-Id (f x))
       ( is-singleton-im-singleton-subtype)
 ```
 

src/foundation/symmetric-identity-types.lagda.md

@@ -67,7 +67,7 @@ module _
       (p : symmetric-Id a) → is-torsorial (Eq-symmetric-Id p)
     is-torsorial-Eq-symmetric-Id (x , H) =
       is-torsorial-Eq-structure
-        ( is-torsorial-path x)
+        ( is-torsorial-Id x)
         ( x , refl)
         ( is-torsorial-htpy H)
 

src/foundation/type-duality.lagda.md

@@ -119,7 +119,7 @@ is-emb-map-type-duality {l} {l1} {A} H (X , f) =
                 ( Σ Y (λ y → type-is-small (H (g y) a)))) ∘e
               ( equiv-univalence))) ∘e
           ( equiv-funext)))
-      ( is-torsorial-path (X , f)))
+      ( is-torsorial-Id (X , f)))
     ( λ Y → ap (map-type-duality H))
 
 emb-type-duality :

src/foundation/univalence.lagda.md

@@ -112,7 +112,7 @@ module _
       is-contr-equiv'
         ( Σ (UU l) (λ X → X ＝ A))
         ( equiv-tot (λ X → equiv-univalence))
-        ( is-torsorial-path' A)
+        ( is-torsorial-Id' A)
 ```
 
 ### Univalence for type families

src/foundation/universal-property-identity-types.lagda.md

@@ -129,7 +129,7 @@ module _
               ( equiv-ev-refl x) ∘e
               ( equiv-inclusion-is-full-subtype
                 ( Π-Prop A ∘ (is-equiv-Prop ∘_))
-                ( fundamental-theorem-id (is-torsorial-path a))) ∘e
+                ( fundamental-theorem-id (is-torsorial-Id a))) ∘e
               ( distributive-Π-Σ))))
         ( emb-tot
           ( λ x →
@@ -145,7 +145,7 @@ module _
         ( λ _ →
           is-injective-emb
             ( emb-fiber-Id-preunivalent-Id a)
-            ( eq-is-contr (is-torsorial-path a))))
+            ( eq-is-contr (is-torsorial-Id a))))
       ( λ _ → ap Id)
 
 module _

src/foundation/universal-property-truncation.lagda.md

@@ -68,7 +68,7 @@ module _
                       ( K x' x)
                       ( Id-Truncated-Type C (g x') z)))) ∘e
               ( equiv-ev-pair)))
-          ( is-torsorial-path (g x)))
+          ( is-torsorial-Id (g x)))
 
   is-truncation-is-truncation-ap :
     is-truncation B f

src/foundation/weak-function-extensionality.lagda.md

@@ -101,7 +101,7 @@ abstract
           ( λ t → eq-pair-Σ refl refl))
         ( weak-funext A
           ( λ x → Σ (B x) (λ b → f x ＝ b))
-          ( λ x → is-torsorial-path (f x))))
+          ( λ x → is-torsorial-Id (f x))))
       ( λ g → htpy-eq {g = g})
 ```