review

src/foundation/action-on-identifications-binary-functions.lagda.md

@@ -31,7 +31,7 @@ we call this the
 There are a few different ways we can define `ap-binary`. We could define it by
 pattern matching on both `p` and `q`, but this leads to restricted computational
 behaviour. Instead, we define it as the upper concatenation in the Gray
-interchange diagram
+interchanger diagram
 
 ```text
                       ap (r ↦ f x r) q

src/foundation/path-algebra.lagda.md

@@ -174,15 +174,15 @@ right-unit-law-vertical-concat-Id² :
   vertical-concat-Id² α refl ＝ α
 right-unit-law-vertical-concat-Id² = right-unit
 
-compute-left-horizontal-concat-Id² :
+compute-left-refl-horizontal-concat-Id² :
   {l : Level} {A : UU l} {x y z : A} {p : x ＝ y} {u v : y ＝ z} (γ : u ＝ v) →
   horizontal-concat-Id² refl γ ＝ left-whisker-concat p γ
-compute-left-horizontal-concat-Id² = left-unit-ap-binary (_∙_)
+compute-left-refl-horizontal-concat-Id² = left-unit-ap-binary (_∙_)
 
-compute-right-horizontal-concat-Id² :
+compute-right-refl-horizontal-concat-Id² :
   {l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} (α : p ＝ q) {u : y ＝ z} →
   horizontal-concat-Id² α refl ＝ right-whisker-concat α u
-compute-right-horizontal-concat-Id² = right-unit-ap-binary (_∙_)
+compute-right-refl-horizontal-concat-Id² = right-unit-ap-binary (_∙_)
 ```
 
 Horizontal concatenation satisfies an additional "2-dimensional" unit law (on
@@ -202,7 +202,9 @@ module _
   nat-sq-right-unit-Id² =
     ( ( horizontal-concat-Id² refl (inv (ap-id α))) ∙
       ( nat-htpy htpy-right-unit α)) ∙
-    ( horizontal-concat-Id² (inv (compute-right-horizontal-concat-Id² α)) refl)
+    ( horizontal-concat-Id²
+      ( inv (compute-right-refl-horizontal-concat-Id² α))
+      ( refl))
 
   nat-sq-left-unit-Id² :
     coherence-square-identifications
@@ -212,7 +214,7 @@ module _
       ( α)
   nat-sq-left-unit-Id² =
     ( ( (inv (ap-id α) ∙ (nat-htpy htpy-left-unit α)) ∙ right-unit) ∙
-      ( inv (compute-left-horizontal-concat-Id² α))) ∙
+      ( inv (compute-left-refl-horizontal-concat-Id² α))) ∙
     ( inv right-unit)
 ```
 
@@ -289,20 +291,22 @@ inner-interchange-Id² :
   (β : p ＝ r) (γ : u ＝ v) →
   ( horizontal-concat-Id² β γ) ＝
   ( vertical-concat-Id² (left-whisker-concat p γ) (right-whisker-concat β v))
-inner-interchange-Id² {u = refl} β refl = compute-right-horizontal-concat-Id² β
+inner-interchange-Id² {u = refl} β refl =
+  compute-right-refl-horizontal-concat-Id² β
 
 outer-interchange-Id² :
   {l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u w : y ＝ z}
   (α : p ＝ q) (δ : u ＝ w) →
   ( horizontal-concat-Id² α δ) ＝
   ( vertical-concat-Id² (right-whisker-concat α u) (left-whisker-concat q δ))
-outer-interchange-Id² {p = refl} refl δ = compute-left-horizontal-concat-Id² δ
+outer-interchange-Id² {p = refl} refl δ =
+  compute-left-refl-horizontal-concat-Id² δ
 
 unit-law-α-interchange-Id² :
   {l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} (α : p ＝ q) (u : y ＝ z) →
   ( ( interchange-Id² α refl (refl {x = u}) refl) ∙
-    ( right-unit ∙ compute-right-horizontal-concat-Id² α)) ＝
-  ( ( compute-right-horizontal-concat-Id² (α ∙ refl)) ∙
+    ( right-unit ∙ compute-right-refl-horizontal-concat-Id² α)) ＝
+  ( ( compute-right-refl-horizontal-concat-Id² (α ∙ refl)) ∙
     ( ap (λ s → right-whisker-concat s u) right-unit))
 unit-law-α-interchange-Id² refl _ = refl
 
@@ -314,8 +318,8 @@ unit-law-β-interchange-Id² refl _ = refl
 unit-law-γ-interchange-Id² :
   {l : Level} {A : UU l} {x y z : A} (p : x ＝ y) {u v : y ＝ z} (γ : u ＝ v) →
   ( ( interchange-Id² (refl {x = p}) refl γ refl) ∙
-    ( right-unit ∙ compute-left-horizontal-concat-Id² γ)) ＝
-  ( ( compute-left-horizontal-concat-Id² (γ ∙ refl)) ∙
+    ( right-unit ∙ compute-left-refl-horizontal-concat-Id² γ)) ＝
+  ( ( compute-left-refl-horizontal-concat-Id² (γ ∙ refl)) ∙
     ( ap (left-whisker-concat p) right-unit))
 unit-law-γ-interchange-Id² _ refl = refl
 
@@ -387,13 +391,13 @@ left-unit-law-y-concat-Id³ :
   {l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} {α : p ＝ q} {γ δ : q ＝ r}
   {τ : γ ＝ δ} →
   y-concat-Id³ (refl {x = α}) τ ＝ left-whisker-concat α τ
-left-unit-law-y-concat-Id³ {τ = τ} = compute-left-horizontal-concat-Id² τ
+left-unit-law-y-concat-Id³ {τ = τ} = compute-left-refl-horizontal-concat-Id² τ
 
 right-unit-law-y-concat-Id³ :
   {l : Level} {A : UU l} {x y : A} {p q r : x ＝ y} {α β : p ＝ q} {γ : q ＝ r}
   {σ : α ＝ β} →
   y-concat-Id³ σ (refl {x = γ}) ＝ right-whisker-concat σ γ
-right-unit-law-y-concat-Id³ {σ = σ} = compute-right-horizontal-concat-Id² σ
+right-unit-law-y-concat-Id³ {σ = σ} = compute-right-refl-horizontal-concat-Id² σ
 
 left-unit-law-z-concat-Id³ :
   {l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z}

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

@@ -709,7 +709,7 @@ module _
 ### Action of binary functions on Yoneda identifications
 
 We obtain an action of binary functions on Yoneda identifications that computes
-on both arguments using one of the two sides in the Gray interchange diagram
+on both arguments using one of the two sides in the Gray interchanger diagram
 
 ```text
                       ap (r ↦ f x r) q

src/synthetic-homotopy-theory/double-loop-spaces.lagda.md

@@ -81,7 +81,7 @@ module _
     {a : A} {α : type-Ω² a} →
     horizontal-concat-Ω² refl-Ω² α ＝ α
   left-unit-law-horizontal-concat-Ω² {α = α} =
-    compute-left-horizontal-concat-Id² α ∙ ap-id α
+    compute-left-refl-horizontal-concat-Id² α ∙ ap-id α
 
   naturality-right-unit :
     {x y : A} {p q : x ＝ y} (α : p ＝ q) →
@@ -99,7 +99,7 @@ module _
   right-unit-law-horizontal-concat-Ω² :
     {a : A} {α : type-Ω² a} → horizontal-concat-Ω² α refl-Ω² ＝ α
   right-unit-law-horizontal-concat-Ω² {α = α} =
-    compute-right-horizontal-concat-Id² α ∙ naturality-right-unit-Ω² α
+    compute-right-refl-horizontal-concat-Id² α ∙ naturality-right-unit-Ω² α
 
   left-unit-law-left-whisker-Ω² :
     {a : A} (α : type-Ω² a) → left-whisker-concat (refl-Ω (A , a)) α ＝ α

src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md

@@ -106,7 +106,7 @@ left-unit-law-z-concat-Ω³ :
 left-unit-law-z-concat-Ω³ α =
   ( left-unit-law-z-concat-Id³ α) ∙
   ( ( inv right-unit) ∙
-    ( ( inv-nat-htpy (λ ω → compute-left-horizontal-concat-Id² ω) α) ∙
+    ( ( inv-nat-htpy (λ ω → compute-left-refl-horizontal-concat-Id² ω) α) ∙
       ( ( inv right-unit) ∙
         ( ( inv-nat-htpy ap-id α) ∙
           ( ap-id α)))))
@@ -129,7 +129,7 @@ right-unit-law-z-concat-Ω³ α =
 -}
 {-
   ( ( inv right-unit) ∙
-    ( ( inv-nat-htpy (λ ω → compute-right-horizontal-concat-Id² ω) α) ∙
+    ( ( inv-nat-htpy (λ ω → compute-right-refl-horizontal-concat-Id² ω) α) ∙
       ( left-unit ∙
         ( ( inv right-unit) ∙
           ( ( inv-nat-htpy