diff --git a/src/category-theory/groupoids.lagda.md b/src/category-theory/groupoids.lagda.md
index de26e339b3..7028c7da72 100644
--- a/src/category-theory/groupoids.lagda.md
+++ b/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)
diff --git a/src/category-theory/isomorphisms-in-categories.lagda.md b/src/category-theory/isomorphisms-in-categories.lagda.md
index b80829fa85..5efbcdb841 100644
--- a/src/category-theory/isomorphisms-in-categories.lagda.md
+++ b/src/category-theory/isomorphisms-in-categories.lagda.md
@@ -743,7 +743,7 @@ 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)
@@ -751,7 +751,7 @@ module _
     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`
diff --git a/src/category-theory/isomorphisms-in-large-categories.lagda.md b/src/category-theory/isomorphisms-in-large-categories.lagda.md
index cfa72bca82..e6f13cb68a 100644
--- a/src/category-theory/isomorphisms-in-large-categories.lagda.md
+++ b/src/category-theory/isomorphisms-in-large-categories.lagda.md
@@ -199,7 +199,7 @@ 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)
@@ -207,7 +207,7 @@ module _
     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
diff --git a/src/category-theory/slice-precategories.lagda.md b/src/category-theory/slice-precategories.lagda.md
index 2e0eb5f494..101b4b7712 100644
--- a/src/category-theory/slice-precategories.lagda.md
+++ b/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
diff --git a/src/elementary-number-theory/universal-property-integers.lagda.md b/src/elementary-number-theory/universal-property-integers.lagda.md
index 3602311b47..a8689cf3e8 100644
--- a/src/elementary-number-theory/universal-property-integers.lagda.md
+++ b/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)))
diff --git a/src/elementary-number-theory/universal-property-natural-numbers.lagda.md b/src/elementary-number-theory/universal-property-natural-numbers.lagda.md
index 9044063f8b..5edeebe5cc 100644
--- a/src/elementary-number-theory/universal-property-natural-numbers.lagda.md
+++ b/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))))
 
diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md
index 3d2821c664..afb4ad31b8 100644
--- a/src/foundation-core/contractible-types.lagda.md
+++ b/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
diff --git a/src/foundation/embeddings.lagda.md b/src/foundation/embeddings.lagda.md
index 8a4e18fbe5..49b66be7e3 100644
--- a/src/foundation/embeddings.lagda.md
+++ b/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
diff --git a/src/foundation/equality-coproduct-types.lagda.md b/src/foundation/equality-coproduct-types.lagda.md
index 6252418e66..ea0ad0ca29 100644
--- a/src/foundation/equality-coproduct-types.lagda.md
+++ b/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)
diff --git a/src/foundation/families-of-maps.lagda.md b/src/foundation/families-of-maps.lagda.md
index 94ab9ec72e..79070bc5ac 100644
--- a/src/foundation/families-of-maps.lagda.md
+++ 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 , _) →
diff --git a/src/foundation/functional-correspondences.lagda.md b/src/foundation/functional-correspondences.lagda.md
index dcc17b0b4b..7bf1fe2d0c 100644
--- a/src/foundation/functional-correspondences.lagda.md
+++ b/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)
diff --git a/src/foundation/fundamental-theorem-of-identity-types.lagda.md b/src/foundation/fundamental-theorem-of-identity-types.lagda.md
index 57fa70fa94..9614810977 100644
--- a/src/foundation/fundamental-theorem-of-identity-types.lagda.md
+++ b/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)) →
diff --git a/src/foundation/homotopy-induction.lagda.md b/src/foundation/homotopy-induction.lagda.md
index 4c35f92ee6..da645df1f2 100644
--- a/src/foundation/homotopy-induction.lagda.md
+++ b/src/foundation/homotopy-induction.lagda.md
@@ -90,7 +90,7 @@ 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)
@@ -98,7 +98,7 @@ module _
       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
diff --git a/src/foundation/images.lagda.md b/src/foundation/images.lagda.md
index ac7b172c3c..f678e73231 100644
--- a/src/foundation/images.lagda.md
+++ b/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)
diff --git a/src/foundation/logical-equivalences.lagda.md b/src/foundation/logical-equivalences.lagda.md
index 4df5fd6e56..b6cbf82ad8 100644
--- a/src/foundation/logical-equivalences.lagda.md
+++ b/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
diff --git a/src/foundation/multivariable-homotopies.lagda.md b/src/foundation/multivariable-homotopies.lagda.md
index 48783bc3f8..49f9ff4882 100644
--- a/src/foundation/multivariable-homotopies.lagda.md
+++ b/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 :
diff --git a/src/foundation/pairs-of-distinct-elements.lagda.md b/src/foundation/pairs-of-distinct-elements.lagda.md
index 92ad06dd75..8b152f6408 100644
--- a/src/foundation/pairs-of-distinct-elements.lagda.md
+++ b/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)
diff --git a/src/foundation/partitions.lagda.md b/src/foundation/partitions.lagda.md
index 220e28ce32..9f37022516 100644
--- a/src/foundation/partitions.lagda.md
+++ b/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
diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md
index 64af30d769..2f4d48bdf0 100644
--- a/src/foundation/pullbacks.lagda.md
+++ b/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))
 ```
 
diff --git a/src/foundation/russells-paradox.lagda.md b/src/foundation/russells-paradox.lagda.md
index a3552d5d08..d4ac4625c8 100644
--- a/src/foundation/russells-paradox.lagda.md
+++ b/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
diff --git a/src/foundation/sections.lagda.md b/src/foundation/sections.lagda.md
index 7854512e21..86de6b12bb 100644
--- a/src/foundation/sections.lagda.md
+++ b/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-Π-Σ))
diff --git a/src/foundation/sequential-limits.lagda.md b/src/foundation/sequential-limits.lagda.md
index 3910a4a89b..c01524227e 100644
--- a/src/foundation/sequential-limits.lagda.md
+++ b/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) →
diff --git a/src/foundation/singleton-subtypes.lagda.md b/src/foundation/singleton-subtypes.lagda.md
index c8d010b9ae..ed53f6dc71 100644
--- a/src/foundation/singleton-subtypes.lagda.md
+++ b/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)
 ```
 
diff --git a/src/foundation/symmetric-identity-types.lagda.md b/src/foundation/symmetric-identity-types.lagda.md
index 0f1282b7e5..4390404734 100644
--- a/src/foundation/symmetric-identity-types.lagda.md
+++ b/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)
 
diff --git a/src/foundation/type-duality.lagda.md b/src/foundation/type-duality.lagda.md
index 9010140341..bf363dbedf 100644
--- a/src/foundation/type-duality.lagda.md
+++ b/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 :
diff --git a/src/foundation/univalence.lagda.md b/src/foundation/univalence.lagda.md
index 1df7bab84c..1e7f3190b7 100644
--- a/src/foundation/univalence.lagda.md
+++ b/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
diff --git a/src/foundation/universal-property-identity-types.lagda.md b/src/foundation/universal-property-identity-types.lagda.md
index af544782f6..74679cffd1 100644
--- a/src/foundation/universal-property-identity-types.lagda.md
+++ b/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 _
diff --git a/src/foundation/universal-property-truncation.lagda.md b/src/foundation/universal-property-truncation.lagda.md
index 2df1545015..80dec71320 100644
--- a/src/foundation/universal-property-truncation.lagda.md
+++ b/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
diff --git a/src/foundation/weak-function-extensionality.lagda.md b/src/foundation/weak-function-extensionality.lagda.md
index cfd66c65ae..c445141e12 100644
--- a/src/foundation/weak-function-extensionality.lagda.md
+++ b/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})
 ```
 
diff --git a/src/graph-theory/equivalences-directed-graphs.lagda.md b/src/graph-theory/equivalences-directed-graphs.lagda.md
index 726b7fb471..ec10cf5c03 100644
--- a/src/graph-theory/equivalences-directed-graphs.lagda.md
+++ b/src/graph-theory/equivalences-directed-graphs.lagda.md
@@ -335,7 +335,7 @@ module _
     is-contr-equiv'
       ( Σ (Directed-Graph l1 l2) (λ H → G ＝ H))
       ( equiv-tot extensionality-Directed-Graph)
-      ( is-torsorial-path G)
+      ( is-torsorial-Id G)
 ```
 
 ### The inverse of an equivalence of directed trees
diff --git a/src/graph-theory/fibers-directed-graphs.lagda.md b/src/graph-theory/fibers-directed-graphs.lagda.md
index cf20c1a1bf..7f0d16753a 100644
--- a/src/graph-theory/fibers-directed-graphs.lagda.md
+++ b/src/graph-theory/fibers-directed-graphs.lagda.md
@@ -200,7 +200,7 @@ module _
     direct-predecessor-Directed-Graph G
       ( node-inclusion-fiber-Directed-Graph G x y)
   compute-direct-predecessor-fiber-Directed-Graph y =
-    ( right-unit-law-Σ-is-contr (λ (u , e) → is-torsorial-path' _)) ∘e
+    ( right-unit-law-Σ-is-contr (λ (u , e) → is-torsorial-Id' _)) ∘e
     ( interchange-Σ-Σ _)
 
   map-compute-direct-predecessor-fiber-Directed-Graph :
diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md
index cd6f407532..822b9d4c23 100644
--- a/src/graph-theory/walks-directed-graphs.lagda.md
+++ b/src/graph-theory/walks-directed-graphs.lagda.md
@@ -407,7 +407,7 @@ module _
     is-contr-equiv'
       ( Σ (vertex-Directed-Graph G) (λ y → y ＝ x))
       ( equiv-tot (λ y → compute-raise l2 (y ＝ x)))
-      ( is-torsorial-path' x)
+      ( is-torsorial-Id' x)
 ```
 
 ### `cons-walk e w ≠ refl-walk`
diff --git a/src/graph-theory/walks-undirected-graphs.lagda.md b/src/graph-theory/walks-undirected-graphs.lagda.md
index 0377bd1cc9..52490662e6 100644
--- a/src/graph-theory/walks-undirected-graphs.lagda.md
+++ b/src/graph-theory/walks-undirected-graphs.lagda.md
@@ -169,7 +169,7 @@ module _
     is-contr
       ( vertex-on-walk-Undirected-Graph G (refl-walk-Undirected-Graph {x = x}))
   is-contr-vertex-on-walk-refl-walk-Undirected-Graph =
-    is-torsorial-path x
+    is-torsorial-Id x
 ```
 
 ### The type of vertices on a walk is equivalent to `Fin (n + 1)` where `n` is the length of the walk
@@ -192,7 +192,7 @@ module _
     ( equiv-coprod
       ( compute-vertex-on-walk-Undirected-Graph w)
       ( equiv-is-contr
-        ( is-torsorial-path (other-element-unordered-pair p y))
+        ( is-torsorial-Id (other-element-unordered-pair p y))
         ( is-contr-unit))) ∘e
     ( left-distributive-Σ-coprod
       ( vertex-Undirected-Graph G)
@@ -231,7 +231,7 @@ module _
     ( equiv-coprod
       ( compute-edge-on-walk-Undirected-Graph w)
       ( equiv-is-contr
-        ( is-torsorial-path (pair p e))
+        ( is-torsorial-Id (pair p e))
         ( is-contr-unit))) ∘e
     ( left-distributive-Σ-coprod
       ( total-edge-Undirected-Graph G)
diff --git a/src/group-theory/automorphism-groups.lagda.md b/src/group-theory/automorphism-groups.lagda.md
index 66a609eded..aa5a4f79ff 100644
--- a/src/group-theory/automorphism-groups.lagda.md
+++ b/src/group-theory/automorphism-groups.lagda.md
@@ -120,7 +120,7 @@ module _
     is-torsorial (Eq-classifying-type-Automorphism-∞-Group X)
   is-torsorial-Eq-classifying-type-Automorphism-∞-Group X =
     is-torsorial-Eq-subtype
-      ( is-torsorial-path (pr1 X))
+      ( is-torsorial-Id (pr1 X))
       ( λ a → is-prop-type-trunc-Prop)
       ( pr1 X)
       ( refl)
diff --git a/src/group-theory/isomorphisms-abelian-groups.lagda.md b/src/group-theory/isomorphisms-abelian-groups.lagda.md
index 7d636cd570..9d7b07d36e 100644
--- a/src/group-theory/isomorphisms-abelian-groups.lagda.md
+++ b/src/group-theory/isomorphisms-abelian-groups.lagda.md
@@ -196,7 +196,7 @@ abstract
     is-contr-equiv'
       ( Σ (Ab l) (Id A))
       ( equiv-tot (equiv-iso-eq-Ab' A))
-      ( is-torsorial-path A)
+      ( is-torsorial-Id A)
 
 is-equiv-iso-eq-Ab :
   {l : Level} (A B : Ab l) → is-equiv (iso-eq-Ab A B)
diff --git a/src/group-theory/isomorphisms-groups.lagda.md b/src/group-theory/isomorphisms-groups.lagda.md
index a176295cd3..0ab46ae767 100644
--- a/src/group-theory/isomorphisms-groups.lagda.md
+++ b/src/group-theory/isomorphisms-groups.lagda.md
@@ -242,7 +242,7 @@ module _
       is-contr-equiv'
         ( Σ (Group l) (Id G))
         ( equiv-tot extensionality-Group')
-        ( is-torsorial-path G)
+        ( is-torsorial-Id G)
 ```
 
 ### Group isomorphisms are stable by composition
diff --git a/src/group-theory/orbits-monoid-actions.lagda.md b/src/group-theory/orbits-monoid-actions.lagda.md
index 3238837f89..a6766ac596 100644
--- a/src/group-theory/orbits-monoid-actions.lagda.md
+++ b/src/group-theory/orbits-monoid-actions.lagda.md
@@ -81,7 +81,7 @@ module _
     is-torsorial (htpy-hom-orbit-action-Monoid f)
   is-torsorial-htpy-hom-orbit-action-Monoid {x} {y} f =
     is-torsorial-Eq-subtype
-      ( is-torsorial-path (element-hom-orbit-action-Monoid f))
+      ( is-torsorial-Id (element-hom-orbit-action-Monoid f))
       ( λ u →
         is-set-type-action-Monoid M X (mul-action-Monoid M X u x) y)
       ( element-hom-orbit-action-Monoid f)
diff --git a/src/lists/lists.lagda.md b/src/lists/lists.lagda.md
index 82634d6451..70c2f61bc6 100644
--- a/src/lists/lists.lagda.md
+++ b/src/lists/lists.lagda.md
@@ -220,7 +220,7 @@ is-torsorial-Eq-list {A = A} l =
   is-contr-equiv'
     ( Σ (list A) (Id l))
     ( equiv-tot (equiv-Eq-list l))
-    ( is-torsorial-path l)
+    ( is-torsorial-Id l)
 
 is-trunc-Eq-list :
   (k : 𝕋) {l : Level} {A : UU l} → is-trunc (succ-𝕋 (succ-𝕋 k)) A →
diff --git a/src/orthogonal-factorization-systems/closed-modalities.lagda.md b/src/orthogonal-factorization-systems/closed-modalities.lagda.md
index 7c79d77436..bdbd345410 100644
--- a/src/orthogonal-factorization-systems/closed-modalities.lagda.md
+++ b/src/orthogonal-factorization-systems/closed-modalities.lagda.md
@@ -90,7 +90,7 @@ module _
                         ( f' a)
                         ( center (is-modal-B q))))) ∘e
               ( equiv-up-join B)))
-          ( is-torsorial-path' f))
+          ( is-torsorial-Id' f))
 
   reflective-subuniverse-closed-modality :
     reflective-subuniverse (l ⊔ lQ) (l ⊔ lQ)
diff --git a/src/ring-theory/isomorphisms-rings.lagda.md b/src/ring-theory/isomorphisms-rings.lagda.md
index b8575bd7c4..3b76b3ef97 100644
--- a/src/ring-theory/isomorphisms-rings.lagda.md
+++ b/src/ring-theory/isomorphisms-rings.lagda.md
@@ -491,7 +491,7 @@ module _
             ( (mul-Ring R , associative-mul-Ring R) , λ {x} {y} → refl)
             ( is-torsorial-Eq-subtype
               ( is-torsorial-Eq-subtype
-                ( is-torsorial-path (one-Ring R))
+                ( is-torsorial-Id (one-Ring R))
                 ( λ x →
                   is-prop-prod
                     ( is-prop-Π (λ y → is-set-type-Ring R (mul-Ring R x y) y))
diff --git a/src/structured-types/pointed-equivalences.lagda.md b/src/structured-types/pointed-equivalences.lagda.md
index 0c24aaae98..80c212d416 100644
--- a/src/structured-types/pointed-equivalences.lagda.md
+++ b/src/structured-types/pointed-equivalences.lagda.md
@@ -165,7 +165,7 @@ module _
     is-torsorial-Eq-structure
       ( is-torsorial-equiv (type-Pointed-Type A))
       ( pair (type-Pointed-Type A) id-equiv)
-      ( is-torsorial-path (point-Pointed-Type A))
+      ( is-torsorial-Id (point-Pointed-Type A))
 
   extensionality-Pointed-Type : (B : Pointed-Type l1) → Id A B ≃ (A ≃∗ B)
   extensionality-Pointed-Type =
diff --git a/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md b/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md
index c4e36e99ce..83f24fc993 100644
--- a/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md
+++ b/src/structured-types/pointed-types-equipped-with-automorphisms.lagda.md
@@ -159,7 +159,7 @@ is-torsorial-htpy-hom-Pointed-Type-With-Aut X Y h1 =
     ( is-torsorial-htpy (map-hom-Pointed-Type-With-Aut X Y h1))
     ( pair (map-hom-Pointed-Type-With-Aut X Y h1) refl-htpy)
     ( is-torsorial-Eq-structure
-      ( is-torsorial-path
+      ( is-torsorial-Id
         ( preserves-point-map-hom-Pointed-Type-With-Aut X Y h1))
       ( pair (preserves-point-map-hom-Pointed-Type-With-Aut X Y h1) refl)
       ( is-contr-equiv'
diff --git a/src/structured-types/pointed-universal-property-contractible-types.lagda.md b/src/structured-types/pointed-universal-property-contractible-types.lagda.md
index 3c595d66c6..93bb61ec11 100644
--- a/src/structured-types/pointed-universal-property-contractible-types.lagda.md
+++ b/src/structured-types/pointed-universal-property-contractible-types.lagda.md
@@ -73,7 +73,7 @@ module _
     is-contr-equiv
       ( Σ X (λ y → y ＝ x))
       ( equiv-Σ-equiv-base _ (equiv-universal-property-contr a c X))
-      ( is-torsorial-path' x)
+      ( is-torsorial-Id' x)
 
 module _
   {l1 : Level} {A : UU l1}
@@ -101,7 +101,7 @@ module _
           ( equivalence-reasoning
               (A → X)
               ≃ Σ (A → X) (λ f → Σ X (λ x → f a ＝ x))
-                by inv-right-unit-law-Σ-is-contr (λ f → is-torsorial-path (f a))
+                by inv-right-unit-law-Σ-is-contr (λ f → is-torsorial-Id (f a))
               ≃ Σ X (λ x → (A , a) →∗ (X , x))
                 by equiv-left-swap-Σ
               ≃ X
@@ -110,7 +110,7 @@ module _
               ap
                 ( pr1)
                 ( inv
-                  ( contraction (is-torsorial-path (f a)) (pair (f a) refl)))))
+                  ( contraction (is-torsorial-Id (f a)) (pair (f a) refl)))))
 
 module _
   {l1 : Level} (A : Pointed-Type l1)
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index 2d2b34123b..b09342fe44 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -376,7 +376,7 @@ module _
           equiv-left-swap-Σ
       ≃ (C → X)
         by
-          equiv-pr1 (λ v → is-torsorial-path' (v ∘ horizontal-map-cocone f g c))
+          equiv-pr1 (λ v → is-torsorial-Id' (v ∘ horizontal-map-cocone f g c))
 
   is-acyclic-map-vertical-map-cocone-is-pushout :
     is-pushout f g c →
diff --git a/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md b/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md
index ba96029837..40f331bb0d 100644
--- a/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md
@@ -104,15 +104,15 @@ module _
       ( unit)
       ( inv-equiv
         ( terminal-map (fiber id b) ,
-        ( is-equiv-terminal-map-is-contr (is-torsorial-path' b))))
+        ( is-equiv-terminal-map-is-contr (is-torsorial-Id' b))))
       ( inv-equiv
         ( terminal-map (fiber id b) ,
-          ( is-equiv-terminal-map-is-contr (is-torsorial-path' b))))
+          ( is-equiv-terminal-map-is-contr (is-torsorial-Id' b))))
       ( id-equiv)
       ( terminal-map (fiber f b))
       ( terminal-map (fiber f b))
-      ( λ _ → eq-is-contr (is-torsorial-path' b))
-      ( λ _ → eq-is-contr (is-torsorial-path' b))
+      ( λ _ → eq-is-contr (is-torsorial-Id' b))
+      ( λ _ → eq-is-contr (is-torsorial-Id' b))
 
   suspension-cocone-fiber :
     suspension-cocone (fiber f b) (fiber (codiagonal-map f) b)
diff --git a/src/synthetic-homotopy-theory/free-loops.lagda.md b/src/synthetic-homotopy-theory/free-loops.lagda.md
index 179b0d76fa..9abf11b695 100644
--- a/src/synthetic-homotopy-theory/free-loops.lagda.md
+++ b/src/synthetic-homotopy-theory/free-loops.lagda.md
@@ -95,14 +95,14 @@ module _
       (α : free-loop X) → is-torsorial (Eq-free-loop α)
     is-torsorial-Eq-free-loop (pair x α) =
       is-torsorial-Eq-structure
-        ( is-torsorial-path x)
+        ( is-torsorial-Id x)
         ( pair x refl)
         ( is-contr-is-equiv'
           ( Σ (Id x x) (λ α' → Id α α'))
           ( tot (λ α' α → right-unit ∙ α))
           ( is-equiv-tot-is-fiberwise-equiv
             ( λ α' → is-equiv-concat right-unit α'))
-          ( is-torsorial-path α))
+          ( is-torsorial-Id α))
 
   abstract
     is-equiv-Eq-eq-free-loop :
@@ -142,14 +142,14 @@ module _
       ( p : free-dependent-loop α P) → is-torsorial (Eq-free-dependent-loop p)
     is-torsorial-Eq-free-dependent-loop (pair y p) =
       is-torsorial-Eq-structure
-        ( is-torsorial-path y)
+        ( is-torsorial-Id y)
         ( pair y refl)
         ( is-contr-is-equiv'
           ( Σ (Id (tr P (loop-free-loop α) y) y) (λ p' → Id p p'))
           ( tot (λ p' α → right-unit ∙ α))
           ( is-equiv-tot-is-fiberwise-equiv
             ( λ p' → is-equiv-concat right-unit p'))
-          ( is-torsorial-path p))
+          ( is-torsorial-Id p))
 
   abstract
     is-equiv-Eq-free-dependent-loop-eq :
diff --git a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
index 7c4a10756d..4f8238af04 100644
--- a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
+++ b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
@@ -153,15 +153,15 @@ module _
     is-torsorial Eq-structure-Hatcher-Acyclic-Type
   is-torsorial-Eq-structure-Hatcher-Acyclic-Type =
     is-torsorial-Eq-structure
-      ( is-torsorial-path (pr1 s))
+      ( is-torsorial-Id (pr1 s))
       ( pr1 s , refl)
       ( is-torsorial-Eq-structure
-        ( is-torsorial-path (pr1 (pr2 s)))
+        ( is-torsorial-Id (pr1 (pr2 s)))
         ( pr1 (pr2 s) , refl)
         ( is-torsorial-Eq-structure
-          ( is-torsorial-path (pr1 (pr2 (pr2 s)) ∙ refl))
+          ( is-torsorial-Id (pr1 (pr2 (pr2 s)) ∙ refl))
           ( pr1 (pr2 (pr2 s)) , right-unit)
-          ( is-torsorial-path (pr2 (pr2 (pr2 s)) ∙ refl))))
+          ( is-torsorial-Id (pr2 (pr2 (pr2 s)) ∙ refl))))
 
   Eq-eq-structure-Hatcher-Acyclic-Type :
     (t : structure-Hatcher-Acyclic-Type A) →
@@ -216,7 +216,7 @@ module _
               ( ( inv (power-nat-mul-Ω 3 2 (Ω A) a)) ∙
                 ( power-nat-succ-Ω' 5 (Ω A) a)))) ∘e
           ( ( ( left-unit-law-Σ-is-contr
-                ( is-torsorial-path' (a ∙ a))
+                ( is-torsorial-Id' (a ∙ a))
                 ( a ∙ a , refl)) ∘e
               ( inv-associative-Σ
                 ( type-Ω (Ω A))
@@ -239,7 +239,7 @@ module _
                     ( equiv-concat'
                       ( power-nat-Ω 3 (Ω A) b)
                       ( interchange-concat-Ω² a b a b)))))))))
-        ( is-torsorial-path refl)
+        ( is-torsorial-Id refl)
 ```
 
 ### For a fixed pointed map, the `is-hom-pointed-map-algebra-Hatcher-Acyclic-Type` family is torsorial
@@ -309,13 +309,13 @@ module _
         is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' (A , σ) (B , τ) f)
   is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' =
     is-torsorial-Eq-structure
-      ( is-torsorial-path (map-Ω f a1)) ((map-Ω f a1) , refl)
+      ( is-torsorial-Id (map-Ω f a1)) ((map-Ω f a1) , refl)
       ( is-torsorial-Eq-structure
-        ( is-torsorial-path (map-Ω f a2)) ((map-Ω f a2) , refl)
+        ( is-torsorial-Id (map-Ω f a2)) ((map-Ω f a2) , refl)
         ( is-torsorial-Eq-structure
-          ( is-torsorial-path _)
+          ( is-torsorial-Id _)
           ( _ , refl)
-          ( is-torsorial-path _)))
+          ( is-torsorial-Id _)))
 
   abstract
     is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type :
diff --git a/src/synthetic-homotopy-theory/suspension-structures.lagda.md b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
index 6a3e59877e..90522d9f5d 100644
--- a/src/synthetic-homotopy-theory/suspension-structures.lagda.md
+++ b/src/synthetic-homotopy-theory/suspension-structures.lagda.md
@@ -268,7 +268,7 @@ module _
           ( Σ (suspension-structure X Z) (λ c' → c ＝ c'))
           ( inv-equiv
             ( equiv-tot (extensionality-suspension-structure c)))
-          ( is-torsorial-path c))
+          ( is-torsorial-Id c))
         ( P))
 ```
 
diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
index ac4e4cb5b7..77461197bb 100644
--- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
@@ -607,7 +607,7 @@ module _
           equiv-left-swap-Σ
       ≃ (C → type-Truncated-Type X)
         by
-          equiv-pr1 (λ v → is-torsorial-path' (v ∘ horizontal-map-cocone f g c))
+          equiv-pr1 (λ v → is-torsorial-Id' (v ∘ horizontal-map-cocone f g c))
 
   is-truncated-acyclic-map-vertical-map-cocone-is-pushout :
     is-pushout f g c →
diff --git a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
index a638e4ea4b..1ed990b712 100644
--- a/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
+++ b/src/synthetic-homotopy-theory/universal-property-suspensions-of-pointed-types.lagda.md
@@ -143,7 +143,7 @@ module _
     (suspension-Pointed-Type X →∗ Y) ≃ (X →∗ Ω Y)
   equiv-transpose-suspension-loop-adjunction =
     ( left-unit-law-Σ-is-contr
-      ( is-torsorial-path (point-Pointed-Type Y))
+      ( is-torsorial-Id (point-Pointed-Type Y))
       ( point-Pointed-Type Y , refl)) ∘e
     ( inv-associative-Σ
       ( type-Pointed-Type Y)
@@ -159,9 +159,9 @@ module _
         Σ ( point-Pointed-Type Y ＝ pr1 z)
           ( λ x → pr2 z (point-Pointed-Type X) ＝ x))) ∘e
     ( inv-right-unit-law-Σ-is-contr
-      ( λ z → is-torsorial-path (pr2 z (point-Pointed-Type X)))) ∘e
+      ( λ z → is-torsorial-Id (pr2 z (point-Pointed-Type X)))) ∘e
     ( left-unit-law-Σ-is-contr
-      ( is-torsorial-path' (point-Pointed-Type Y))
+      ( is-torsorial-Id' (point-Pointed-Type Y))
       ( point-Pointed-Type Y , refl)) ∘e
     ( equiv-right-swap-Σ) ∘e
     ( equiv-Σ-equiv-base
diff --git a/src/trees/equivalences-directed-trees.lagda.md b/src/trees/equivalences-directed-trees.lagda.md
index 3d53b85582..4b3dbd9ecb 100644
--- a/src/trees/equivalences-directed-trees.lagda.md
+++ b/src/trees/equivalences-directed-trees.lagda.md
@@ -443,7 +443,7 @@ module _
     is-contr-equiv'
       ( Σ (Directed-Tree l1 l2) (λ S → T ＝ S))
       ( equiv-tot extensionality-Directed-Tree)
-      ( is-torsorial-path T)
+      ( is-torsorial-Id T)
 ```
 
 ### A morphism of directed trees is an equivalence if it is an equivalence on the nodes
diff --git a/src/trees/equivalences-enriched-directed-trees.lagda.md b/src/trees/equivalences-enriched-directed-trees.lagda.md
index 435594dd57..b4ee4e1da9 100644
--- a/src/trees/equivalences-enriched-directed-trees.lagda.md
+++ b/src/trees/equivalences-enriched-directed-trees.lagda.md
@@ -506,7 +506,7 @@ module _
     is-contr-equiv'
       ( Σ (Enriched-Directed-Tree l3 l4 A B) (λ S → T ＝ S))
       ( equiv-tot extensionality-Enriched-Directed-Tree)
-      ( is-torsorial-path T)
+      ( is-torsorial-Id T)
 ```
 
 ### A morphism of enriched directed trees is an equivalence if it is an equivalence on the nodes
diff --git a/src/trees/fibers-enriched-directed-trees.lagda.md b/src/trees/fibers-enriched-directed-trees.lagda.md
index c4b4fcaa4a..f546f1acf3 100644
--- a/src/trees/fibers-enriched-directed-trees.lagda.md
+++ b/src/trees/fibers-enriched-directed-trees.lagda.md
@@ -99,7 +99,7 @@ module _
     ( interchange-Σ-Σ (λ u e v → v ＝ cons-walk-Directed-Graph e w)) ∘e
     ( ( inv-right-unit-law-Σ-is-contr
         ( λ i →
-          is-torsorial-path' (cons-walk-Directed-Graph (pr2 i) w))) ∘e
+          is-torsorial-Id' (cons-walk-Directed-Graph (pr2 i) w))) ∘e
       ( enrichment-Enriched-Directed-Tree A B T y))
 
   fiber-Enriched-Directed-Tree : Enriched-Directed-Tree (l3 ⊔ l4) (l3 ⊔ l4) A B
@@ -157,7 +157,7 @@ module _
     map-enrichment-fiber-Enriched-Directed-Tree y b
   eq-map-enrichment-fiber-Enriched-Directed-Tree y b w p =
     eq-interchange-Σ-Σ-is-contr _
-      ( is-torsorial-path'
+      ( is-torsorial-Id'
         ( cons-walk-Directed-Graph
           ( edge-enrichment-Enriched-Directed-Tree A B T
             ( node-inclusion-fiber-Enriched-Directed-Tree y)
diff --git a/src/trees/polynomial-endofunctors.lagda.md b/src/trees/polynomial-endofunctors.lagda.md
index 6962ec19ac..398d54325a 100644
--- a/src/trees/polynomial-endofunctors.lagda.md
+++ b/src/trees/polynomial-endofunctors.lagda.md
@@ -71,7 +71,7 @@ module _
     is-torsorial (Eq-type-polynomial-endofunctor x)
   is-torsorial-Eq-type-polynomial-endofunctor (pair x α) =
     is-torsorial-Eq-structure
-      ( is-torsorial-path x)
+      ( is-torsorial-Id x)
       ( pair x refl)
       ( is-torsorial-htpy α)
 
diff --git a/src/trees/rooted-morphisms-directed-trees.lagda.md b/src/trees/rooted-morphisms-directed-trees.lagda.md
index fb82443c30..81c9d5fc01 100644
--- a/src/trees/rooted-morphisms-directed-trees.lagda.md
+++ b/src/trees/rooted-morphisms-directed-trees.lagda.md
@@ -256,5 +256,5 @@ module _
     is-contr-equiv'
       ( Σ (rooted-hom-Directed-Tree S T) (λ g → f ＝ g))
       ( equiv-tot extensionality-rooted-hom-Directed-Tree)
-      ( is-torsorial-path f)
+      ( is-torsorial-Id f)
 ```
diff --git a/src/univalent-combinatorics/2-element-subtypes.lagda.md b/src/univalent-combinatorics/2-element-subtypes.lagda.md
index efafaa64f8..16f26a1213 100644
--- a/src/univalent-combinatorics/2-element-subtypes.lagda.md
+++ b/src/univalent-combinatorics/2-element-subtypes.lagda.md
@@ -129,10 +129,10 @@ module _
     ( equiv-coprod
       ( equiv-is-contr
         ( is-contr-Fin-one-ℕ)
-        ( is-torsorial-path x))
+        ( is-torsorial-Id x))
       ( equiv-is-contr
         ( is-contr-unit)
-        ( is-torsorial-path y)))
+        ( is-torsorial-Id y)))
 
   has-two-elements-type-standard-2-Element-Subtype :
     has-two-elements type-standard-2-Element-Subtype
diff --git a/src/univalent-combinatorics/cartesian-product-types.lagda.md b/src/univalent-combinatorics/cartesian-product-types.lagda.md
index 0ef51f58d3..fa9ee2a64b 100644
--- a/src/univalent-combinatorics/cartesian-product-types.lagda.md
+++ b/src/univalent-combinatorics/cartesian-product-types.lagda.md
@@ -85,7 +85,7 @@ equiv-left-factor :
 equiv-left-factor {l1} {l2} {X} {Y} y =
   ( ( right-unit-law-prod) ∘e
     ( equiv-tot
-      ( λ x → equiv-is-contr (is-torsorial-path' y) is-contr-unit))) ∘e
+      ( λ x → equiv-is-contr (is-torsorial-Id' y) is-contr-unit))) ∘e
   ( associative-Σ X (λ x → Y) (λ t → Id (pr2 t) y))
 
 count-left-factor :
diff --git a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md
index 99211c837f..8e1578953e 100644
--- a/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md
+++ b/src/univalent-combinatorics/counting-dependent-pair-types.lagda.md
@@ -149,7 +149,7 @@ count-fiber-map-section-family :
 count-fiber-map-section-family {l1} {l2} {A} {B} b e f (pair y z) =
   count-equiv'
     ( ( ( left-unit-law-Σ-is-contr
-            ( is-torsorial-path' y)
+            ( is-torsorial-Id' y)
             ( pair y refl)) ∘e
         ( inv-associative-Σ A
           ( λ x → Id x y)
diff --git a/src/univalent-combinatorics/dependent-pair-types.lagda.md b/src/univalent-combinatorics/dependent-pair-types.lagda.md
index 54170fb6ef..288b6e4881 100644
--- a/src/univalent-combinatorics/dependent-pair-types.lagda.md
+++ b/src/univalent-combinatorics/dependent-pair-types.lagda.md
@@ -106,7 +106,7 @@ abstract
                       ( λ (x : A) → Id x (pr1 t))
                       ( λ s → Id (tr B (pr2 s) (b (pr1 s))) (pr2 t))) ∘e
                     ( inv-left-unit-law-Σ-is-contr
-                      ( is-torsorial-path' (pr1 t))
+                      ( is-torsorial-Id' (pr1 t))
                       ( pair (pr1 t) refl))))))
             ( count-Σ e
               ( λ t →
diff --git a/src/univalent-combinatorics/fibers-of-maps.lagda.md b/src/univalent-combinatorics/fibers-of-maps.lagda.md
index 5e5eff6376..434a444727 100644
--- a/src/univalent-combinatorics/fibers-of-maps.lagda.md
+++ b/src/univalent-combinatorics/fibers-of-maps.lagda.md
@@ -113,7 +113,7 @@ abstract
   is-finite-fiber-map-section-family {l1} {l2} {A} {B} b f g (pair y z) =
     is-finite-equiv'
       ( ( ( left-unit-law-Σ-is-contr
-            ( is-torsorial-path' y)
+            ( is-torsorial-Id' y)
             ( pair y refl)) ∘e
           ( inv-associative-Σ A
             ( λ x → Id x y)
diff --git a/src/univalent-combinatorics/finite-types.lagda.md b/src/univalent-combinatorics/finite-types.lagda.md
index 8fdc0f7f01..7ae5f6ef72 100644
--- a/src/univalent-combinatorics/finite-types.lagda.md
+++ b/src/univalent-combinatorics/finite-types.lagda.md
@@ -585,7 +585,7 @@ is-torsorial-equiv-𝔽 {l} X =
   is-contr-equiv'
     ( Σ (𝔽 l) (Id X))
     ( equiv-tot (extensionality-𝔽 X))
-    ( is-torsorial-path X)
+    ( is-torsorial-Id X)
 
 equiv-eq-𝔽 : {l : Level} → (X Y : 𝔽 l) → Id X Y → equiv-𝔽 X Y
 equiv-eq-𝔽 X Y = map-equiv (extensionality-𝔽 X Y)