reflexive-htpy-... -> refl-htpy-...

UniMath · Jan 16, 2024 · e9d7cce · e9d7cce
1 parent 1ea12cc
commit e9d7cce
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 12 deletions.
diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
@@ -203,16 +203,16 @@ module _
   ( c : cocone-sequential-diagram A X)
   where
 
-  reflexive-htpy-cocone-sequential-diagram :
+  refl-htpy-cocone-sequential-diagram :
     htpy-cocone-sequential-diagram c c
-  pr1 reflexive-htpy-cocone-sequential-diagram n = refl-htpy
-  pr2 reflexive-htpy-cocone-sequential-diagram n = right-unit-htpy
+  pr1 refl-htpy-cocone-sequential-diagram n = refl-htpy
+  pr2 refl-htpy-cocone-sequential-diagram n = right-unit-htpy
 
   htpy-eq-cocone-sequential-diagram :
     ( c' : cocone-sequential-diagram A X) → ( c ＝ c') →
     htpy-cocone-sequential-diagram c c'
   htpy-eq-cocone-sequential-diagram .c refl =
-    reflexive-htpy-cocone-sequential-diagram
+    refl-htpy-cocone-sequential-diagram
 
   abstract
     is-torsorial-htpy-cocone-sequential-diagram :

diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md
@@ -191,17 +191,17 @@ module _
   { c : cocone-sequential-diagram A X} (P : X → UU l3)
   where
 
-  reflexive-htpy-dependent-cocone-sequential-diagram :
+  refl-htpy-dependent-cocone-sequential-diagram :
     ( d : dependent-cocone-sequential-diagram c P) →
     htpy-dependent-cocone-sequential-diagram P d d
-  pr1 (reflexive-htpy-dependent-cocone-sequential-diagram d) n = refl-htpy
-  pr2 (reflexive-htpy-dependent-cocone-sequential-diagram d) n = right-unit-htpy
+  pr1 (refl-htpy-dependent-cocone-sequential-diagram d) n = refl-htpy
+  pr2 (refl-htpy-dependent-cocone-sequential-diagram d) n = right-unit-htpy
 
   htpy-eq-dependent-cocone-sequential-diagram :
     ( d d' : dependent-cocone-sequential-diagram c P) →
     ( d ＝ d') → htpy-dependent-cocone-sequential-diagram P d d'
   htpy-eq-dependent-cocone-sequential-diagram d .d refl =
-    reflexive-htpy-dependent-cocone-sequential-diagram d
+    refl-htpy-dependent-cocone-sequential-diagram d
 
   abstract
     is-torsorial-htpy-dependent-cocone-sequential-diagram :

diff --git a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
@@ -228,15 +228,15 @@ module _
   { l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
   where
 
-  reflexive-htpy-hom-sequential-diagram :
+  refl-htpy-hom-sequential-diagram :
     ( f : hom-sequential-diagram A B) → htpy-hom-sequential-diagram B f f
-  pr1 (reflexive-htpy-hom-sequential-diagram f) = ev-pair refl-htpy
-  pr2 (reflexive-htpy-hom-sequential-diagram f) = ev-pair right-unit-htpy
+  pr1 (refl-htpy-hom-sequential-diagram f) = ev-pair refl-htpy
+  pr2 (refl-htpy-hom-sequential-diagram f) = ev-pair right-unit-htpy
 
   htpy-eq-sequential-diagram :
     ( f f' : hom-sequential-diagram A B) →
     ( f ＝ f') → htpy-hom-sequential-diagram B f f'
-  htpy-eq-sequential-diagram f .f refl = reflexive-htpy-hom-sequential-diagram f
+  htpy-eq-sequential-diagram f .f refl = refl-htpy-hom-sequential-diagram f
 
   abstract
     is-torsorial-htpy-sequential-diagram :