Code review cleanup

UniMath · Oct 10, 2023 · 4b517a0 · 4b517a0
1 parent 3eab010
commit 4b517a0
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 14 deletions.
diff --git a/src/foundation/commuting-cubes-of-maps.lagda.md b/src/foundation/commuting-cubes-of-maps.lagda.md
@@ -430,8 +430,8 @@ module _
         ( precomp-bottom-whisk-hA)
         by
         inv-htpy
-          ( horizontal-concat-htpy
-            ( horizontal-concat-htpy
+          ( horizontal-concat-htpy²
+            ( horizontal-concat-htpy²
               ( distributive-precomp-right-whisk-coherence-square-maps W hB h' h
                 ( hD)
                 ( inv-htpy front-left)
@@ -511,11 +511,11 @@ module _
         ( ( (precomp g' W) ·l precomp-front-right-inv) ∙h
           ( precomp-back-right-inv ·r (precomp k W)))
         by
-        horizontal-concat-htpy
+        horizontal-concat-htpy²
           ( distributive-precomp-left-whisk-coherence-square-maps W g' f' k' h'
             ( top)
             ( hD))
-          ( horizontal-concat-htpy
+          ( horizontal-concat-htpy²
             ( distributive-precomp-right-whisk-coherence-square-maps W hC k' k
               ( hD)
               ( inv-htpy front-right)

diff --git a/src/foundation/commuting-squares-of-maps.lagda.md b/src/foundation/commuting-squares-of-maps.lagda.md
@@ -490,10 +490,10 @@ module _
     ( H)
     ( K)
     ( h) =
-    ( compute-comp-htpy-precomp (H ∙h L) K W h) ∙
+    ( compute-concat-htpy-precomp (H ∙h L) K W h) ∙
     ( ap
       ( _∙ precomp-coherence-triangle-maps diagonal-right right top K W h)
-      ( compute-comp-htpy-precomp H L W h))
+      ( compute-concat-htpy-precomp H L W h))
 
   distributive-precomp-coherence-square-comp-htpy-coherence-triangle-maps' :
     { diagonal-left diagonal-right : A → Y} →
@@ -528,10 +528,10 @@ module _
     ( H)
     ( K)
     ( h) =
-    ( compute-comp-htpy-precomp H (L ∙h K) W h) ∙
+    ( compute-concat-htpy-precomp H (L ∙h K) W h) ∙
     ( ap
       ( precomp-coherence-triangle-maps' diagonal-left bottom left H W h ∙_)
-      ( compute-comp-htpy-precomp L K W h))
+      ( compute-concat-htpy-precomp L K W h))
 
   distributive-precomp-coherence-square-comp-coherence-triangles-maps :
     ( diagonal : A → Y) →
@@ -564,5 +564,5 @@ module _
     ( H)
     ( K)
     ( h) =
-    compute-comp-htpy-precomp H K W h
+    compute-concat-htpy-precomp H K W h
 ```
diff --git a/src/foundation/equality-dependent-pair-types.lagda.md b/src/foundation/equality-dependent-pair-types.lagda.md
@@ -130,11 +130,11 @@ module _
   { l1 l2 : Level} {A : UU l1} (B : A → UU l2)
   where
 
-  orthogonal-eq-pair-Σ :
+  triangle-eq-pair-Σ :
     { a a' : A} (p : a ＝ a') →
     { b : B a} {b' : B a'} (q : dependent-identification B p b b') →
     eq-pair-Σ p q ＝ (eq-pair-Σ p refl ∙ eq-pair-Σ refl q)
-  orthogonal-eq-pair-Σ refl q = refl
+  triangle-eq-pair-Σ refl q = refl
 ```
 
 ## See also

diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md
@@ -135,11 +135,11 @@ module _
   { l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (a : A) → B a}
   where
 
-  horizontal-concat-htpy :
+  horizontal-concat-htpy² :
     { H H' : f ~ g} → H ~ H' →
     { K K' : g ~ h} → K ~ K' →
     ( H ∙h K) ~ (H' ∙h K')
-  horizontal-concat-htpy α β x = horizontal-concat-Id² (α x) (β x)
+  horizontal-concat-htpy² α β x = horizontal-concat-Id² (α x) (β x)
 ```
 
 ### Transposing homotopies is an equivalence

diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md
@@ -348,7 +348,7 @@ module _
     ( ap-id
       ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e
         ( s , t))) ∙
-    ( orthogonal-eq-pair-Σ Q
+    ( triangle-eq-pair-Σ Q
       ( coherence-square-cocone f g c s)
       ( inv (pr2 (pr2 e) s t))) ∙
     ( ap