From 73b6f68149aa514952db35b8355849bae43a6570 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Thu, 8 Feb 2024 19:03:33 +0100
Subject: [PATCH 01/14] horizontal concatenation is two-sided unital for the
 yoneda identity types

---
 ...-identifications-binary-functions.lagda.md |  6 +-
 src/foundation/path-algebra.lagda.md          | 12 ++-
 src/foundation/yoneda-identity-types.lagda.md | 85 +++++++++++++++++++
 3 files changed, 93 insertions(+), 10 deletions(-)

diff --git a/src/foundation/action-on-identifications-binary-functions.lagda.md b/src/foundation/action-on-identifications-binary-functions.lagda.md
index 3de92507d4..4930ebf1d7 100644
--- a/src/foundation/action-on-identifications-binary-functions.lagda.md
+++ b/src/foundation/action-on-identifications-binary-functions.lagda.md
@@ -39,7 +39,7 @@ module _
 
   ap-binary :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') → f x y ＝ f x' y'
-  ap-binary refl refl = refl
+  ap-binary {x} {x'} p {y} {y'} q = ap (λ z → f z y) p ∙ ap (f x') q
 ```
 
 ## Properties
@@ -68,7 +68,7 @@ module _
   triangle-ap-binary :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
     ap-binary f p q ＝ ap (λ z → f z y) p ∙ ap (f x') q
-  triangle-ap-binary refl refl = refl
+  triangle-ap-binary _ _ = refl
 
   triangle-ap-binary' :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
@@ -89,7 +89,7 @@ module _
 
   left-unit-ap-binary :
     {x : A} {y y' : B} (q : y ＝ y') → ap-binary f refl q ＝ ap (f x) q
-  left-unit-ap-binary refl = refl
+  left-unit-ap-binary _ = refl
 
   right-unit-ap-binary :
     {x x' : A} (p : x ＝ x') {y : B} → ap-binary f p refl ＝ ap (λ z → f z y) p
diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
index bb110a0312..36ca00877d 100644
--- a/src/foundation/path-algebra.lagda.md
+++ b/src/foundation/path-algebra.lagda.md
@@ -142,7 +142,7 @@ vertical-concat-Id² α β = α ∙ β
 
 horizontal-concat-Id² :
   {l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} {u v : y ＝ z} →
-  p ＝ q → u ＝ v → (p ∙ u) ＝ (q ∙ v)
+  p ＝ q → u ＝ v → p ∙ u ＝ q ∙ v
 horizontal-concat-Id² α β = ap-binary (_∙_) α β
 ```
 
@@ -176,14 +176,12 @@ right-unit-law-vertical-concat-Id² = right-unit
 
 left-unit-law-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 {x = p}) γ ＝
-  left-whisker-concat p γ
+  horizontal-concat-Id² refl γ ＝ left-whisker-concat p γ
 left-unit-law-horizontal-concat-Id² = left-unit-ap-binary (_∙_)
 
 right-unit-law-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 {x = u}) ＝
-  right-whisker-concat α u
+  horizontal-concat-Id² α refl ＝ right-whisker-concat α u
 right-unit-law-horizontal-concat-Id² = right-unit-ap-binary (_∙_)
 ```
 
@@ -208,7 +206,7 @@ module _
 
   nat-sq-left-unit-Id² :
     coherence-square-identifications
-      ( horizontal-concat-Id² (refl {x = refl}) α)
+      ( horizontal-concat-Id² refl α)
       ( left-unit)
       ( left-unit)
       ( α)
@@ -227,7 +225,7 @@ module _
   {l : Level} {A : UU l} {x y : A} {p p' : x ＝ y}
   where
 
-  horizontal-inv-Id² : p ＝ p' → (inv p) ＝ (inv p')
+  horizontal-inv-Id² : p ＝ p' → inv p ＝ inv p'
   horizontal-inv-Id² = ap inv
 ```
 
diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index c5ee6d9b9a..2331817ce2 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -8,6 +8,7 @@ module foundation.yoneda-identity-types where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.action-on-identifications-binary-functions
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.multivariable-homotopies
@@ -705,6 +706,19 @@ module _
         ( inv (commutative-preconcatr-refl-Id-yoneda-Id p q)))
 ```
 
+### Action of binary functions on Yoneda identifications
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B → C)
+  where
+
+  ap-binary-yoneda-Id :
+    {x x' : A} (p : x ＝ʸ x') {y y' : B} (q : y ＝ʸ y') → f x y ＝ʸ f x' y'
+  ap-binary-yoneda-Id {x} {x'} p {y} {y'} q =
+    ap-yoneda-Id (λ z → f z y) p ∙ʸ ap-yoneda-Id (f x') q
+```
+
 ### Transport along Yoneda identifications
 
 ```agda
@@ -772,6 +786,77 @@ module _
   is-equiv-yoneda-eq-equiv = is-equiv-map-equiv equiv-yoneda-eq-equiv
 ```
 
+### Horizontal concatenation of yoneda identifications
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z : A}
+  where
+
+  horizontal-concat-yoneda-Id² :
+    {p q : x ＝ʸ y} → p ＝ʸ q → {u v : y ＝ʸ z} → u ＝ʸ v → p ∙ʸ u ＝ʸ q ∙ʸ v
+  horizontal-concat-yoneda-Id² α β = ap-binary-yoneda-Id (_∙ʸ_) α β
+
+  left-unit-horizontal-concat-yoneda-Id² :
+    {p : x ＝ʸ y} {u v : y ＝ʸ z} (β : u ＝ʸ v) →
+    horizontal-concat-yoneda-Id² reflʸ β ＝ ap-yoneda-Id (p ∙ʸ_) β
+  left-unit-horizontal-concat-yoneda-Id² β = refl
+
+  right-unit-horizontal-concat-yoneda-Id² :
+    {p q : x ＝ʸ y} (α : p ＝ʸ q) {u : y ＝ʸ z} →
+    horizontal-concat-yoneda-Id² α (reflʸ {x = u}) ＝ ap-yoneda-Id (_∙ʸ u) α
+  right-unit-horizontal-concat-yoneda-Id² α = refl
+
+module _
+  {l : Level} {A : UU l} {x y z w : A}
+  where
+
+  assoc-horizontal-concat-yoneda-Id² :
+    {p p' : x ＝ʸ y} (α : p ＝ʸ p')
+    {q q' : y ＝ʸ z} (β : q ＝ʸ q')
+    {r r' : z ＝ʸ w} (γ : r ＝ʸ r') →
+    horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² α β) γ ＝
+    horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ)
+  assoc-horizontal-concat-yoneda-Id² {p} α {q} β γ =
+    ind-yoneda-Id
+      ( λ _ α → horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² α β) γ ＝ horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ))
+        (ind-yoneda-Id
+          ( λ _ β → horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² reflʸ β) γ ＝ horizontal-concat-yoneda-Id² reflʸ (horizontal-concat-yoneda-Id² β γ))
+          ( ind-yoneda-Id (λ _ γ → horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² (reflʸ {x = p}) (reflʸ {x = q})) γ ＝ horizontal-concat-yoneda-Id² (reflʸ {x = p}) (horizontal-concat-yoneda-Id² (reflʸ {x = q}) γ)) refl γ)
+          β) α
+```
+
+### Vertical concatenation of yoneda identifications
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y : A}
+  where
+
+  vertical-concat-yoneda-Id² :
+    {p q r : x ＝ʸ y} → p ＝ʸ q → q ＝ʸ r → p ＝ʸ r
+  vertical-concat-yoneda-Id² α β = α ∙ʸ β
+```
+
+### The interchange law for Yoneda identificatinos
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z : A}
+  where
+
+  -- interchange-yoneda-Id² :
+  --   {p q r : x ＝ʸ y} {u v w : y ＝ʸ z}
+  --   (α : p ＝ʸ q) (β : q ＝ʸ r) (γ : u ＝ʸ v) (δ : v ＝ʸ w) →
+  --   ( horizontal-concat-yoneda-Id²
+  --     ( vertical-concat-yoneda-Id² α β)
+  --     ( vertical-concat-yoneda-Id² γ δ)) ＝
+  --   ( vertical-concat-yoneda-Id²
+  --     ( horizontal-concat-yoneda-Id² α γ)
+  --     ( horizontal-concat-yoneda-Id² β δ))
+  -- interchange-yoneda-Id² α β γ δ = {!   !}
+```
+
 ## See also
 
 - [The strictly involutive identity types](foundation.strictly-involutive-identity-types.md)

From 3dd942c5121e4837d4156bc67e5713a31b180f63 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 9 Feb 2024 11:03:49 +0100
Subject: [PATCH 02/14] better notation

---
 .../computational-identity-types.lagda.md     | 134 +++++++-------
 ...trictly-involutive-identity-types.lagda.md |  46 +++--
 src/foundation/yoneda-identity-types.lagda.md | 163 +++++++++++++-----
 3 files changed, 203 insertions(+), 140 deletions(-)

diff --git a/src/foundation/computational-identity-types.lagda.md b/src/foundation/computational-identity-types.lagda.md
index 2b19a54501..256a877232 100644
--- a/src/foundation/computational-identity-types.lagda.md
+++ b/src/foundation/computational-identity-types.lagda.md
@@ -53,13 +53,13 @@ but using the [Yoneda identity types](foundation.yoneda-identity-types.md)
 (`_＝ʸ_`) as the underlying identity types:
 
 ```text
-  (x ＝ʲ y) := Σ (z : A) ((z ＝ʸ y) × (z ＝ʸ x))
+  (x ＝ʸ y) := (z : A) → (z ＝ x) → (z ＝ y),
 ```
 
-The Yoneda identity types are defined as
+hence, their definition is
 
 ```text
-  (x ＝ʸ y) := (z : A) → (z ＝ x) → (z ＝ y).
+  (x ＝ʲ y) := Σ (z : A) ((z ＝ʸ y) × (z ＝ʸ x)).
 ```
 
 The Yoneda identity types are [equivalent](foundation-core.equivalences.md) to
@@ -71,23 +71,22 @@ laws
 
 - `(p ∙ʲ q) ∙ʲ r ≐ p ∙ʲ (q ∙ʲ r)`
 - `reflʲ ∙ʲ p ≐ p` or `p ∙ʲ reflʲ ≐ p`
-- `inv (inv p) ≐ p`
-- `inv reflʲ ≐ reflʲ`.
+- `invʲ (invʲ p) ≐ p`
+- `invʲ reflʲ ≐ reflʲ`.
 
 While the last three equalities hold by the same computations as for the
-strictly involutive identity types using the fact that `inv reflʸ ≐ reflʸ`,
+strictly involutive identity types using the fact that `invʸ reflʸ ≐ reflʸ`,
 strict associativity relies on the strict associativity of the underlying Yoneda
 identity types. See the file about strictly involutive identity types for
-further details on these computations.
-
-In addition to these strict algebraic laws, we also define a recursion principle
+further details on computations related to the last three equalities. In
+addition to these strict algebraic laws, we also define a recursion principle
 for the computational identity types that computes strictly.
 
 **Note.** The computational identity types do _not_ satisfy the strict laws
 
 - `reflʲ ∙ʲ p ≐ p` and `p ∙ʲ reflʲ ≐ p` simultaneously,
-- `inv p ∙ʲ p ≐ reflʲ`, or
-- `p ∙ʲ inv p ≐ reflʲ`,
+- `invʲ p ∙ʲ p ≐ reflʲ`, or
+- `p ∙ʲ invʲ p ≐ reflʲ`,
 
 and they do not have a strict computation property for their induction
 principle. This boils down to the fact that the Yoneda identity types do not
@@ -116,7 +115,8 @@ module _
 
 ### The computational identity types are equivalent to the Yoneda identity types
 
-Similarly to the strictly involutive identity types, this equivalence is a
+The computational identity types are equivalent to the Yoneda identity types,
+and similarly to the strictly involutive identity types, this equivalence is a
 strict [retraction](foundation-core.retractions.md) and preserves the
 reflexivities strictly.
 
@@ -129,7 +129,7 @@ module _
   computational-eq-yoneda-eq {x} f = (x , f , reflʸ)
 
   yoneda-eq-computational-eq : {x y : A} → x ＝ʲ y → x ＝ʸ y
-  yoneda-eq-computational-eq (z , p , q) = inv-yoneda-Id q ∙ʸ p
+  yoneda-eq-computational-eq (z , p , q) = invʸ q ∙ʸ p
 
   is-retraction-yoneda-eq-computational-eq :
     {x y : A} →
@@ -196,8 +196,9 @@ module _
 
 ### The computational identity types are equivalent to the standard identity types
 
-We define the equivalence as the composite `(x ＝ y) ≃ (x ＝ʸ y) ≃ (x ＝ʲ y)`.
-Since each of these equivalences preserve the groupoid structure weakly so does
+By the composite equivalence `(x ＝ y) ≃ (x ＝ʸ y) ≃ (x ＝ʲ y)`, the
+computational identity types are equivalent to the standard identity types.
+Since each of these equivalences preserve the groupoid structure weakly, so does
 the composite. For the same reason, it preserves the reflexivities strictly.
 
 ```agda
@@ -326,6 +327,8 @@ module _
       ( dependent-universal-property-identity-system-computational-Id B)
 ```
 
+### The strict recursion principle for the computational identity types
+
 Using the fact that the recusion principles of both the Yoneda identity types
 and the strictly involutive identity types can be defined to compute strictly,
 we obtain a strictly computing recursion principle for the computational
@@ -363,8 +366,8 @@ structure satisfies the following algebraic laws strictly
 
 - `(p ∙ʲ q) ∙ʲ r ≐ p ∙ʲ (q ∙ʲ r)`
 - `reflʲ ∙ʲ p ≐ p` or `p ∙ʲ reflʲ ≐ p`
-- `inv (inv p) ≐ p`
-- `inv reflʲ ≐ reflʲ`.
+- `invʲ (invʲ p) ≐ p`
+- `invʲ reflʲ ≐ reflʲ`.
 
 ### Inverting computational identifications
 
@@ -381,18 +384,16 @@ module _
   {l : Level} {A : UU l}
   where
 
-  inv-computational-Id : {x y : A} → x ＝ʲ y → y ＝ʲ x
-  inv-computational-Id (z , p , q) = (z , q , p)
+  invʲ : {x y : A} → x ＝ʲ y → y ＝ʲ x
+  invʲ (z , p , q) = (z , q , p)
 
-  compute-inv-computational-Id-refl :
-    {x : A} →
-    inv-computational-Id (reflʲ {x = x}) ＝
-    reflʲ
-  compute-inv-computational-Id-refl = refl
+  compute-inv-refl-computational-Id :
+    {x : A} → invʲ (reflʲ {x = x}) ＝ reflʲ
+  compute-inv-refl-computational-Id = refl
 
   inv-inv-computational-Id :
     {x y : A} (p : x ＝ʲ y) →
-    inv-computational-Id (inv-computational-Id p) ＝ p
+    invʲ (invʲ p) ＝ p
   inv-inv-computational-Id p = refl
 ```
 
@@ -406,12 +407,12 @@ module _
 
   preserves-inv-computational-eq-eq :
     (p : x ＝ y) →
-    computational-eq-eq (inv p) ＝ inv-computational-Id (computational-eq-eq p)
+    computational-eq-eq (inv p) ＝ invʲ (computational-eq-eq p)
   preserves-inv-computational-eq-eq refl = refl
 
   preserves-inv-eq-computational-eq :
     (p : x ＝ʲ y) →
-    eq-computational-eq (inv-computational-Id p) ＝ inv (eq-computational-eq p)
+    eq-computational-eq (invʲ p) ＝ inv (eq-computational-eq p)
   preserves-inv-eq-computational-eq (z , f , g) =
     ( ap (g y) (left-unit-right-strict-concat)) ∙
     ( distributive-inv-Id-yoneda-Id g f) ∙
@@ -421,14 +422,12 @@ module _
 ### The concatenation operations on computational identifications
 
 There is both a strictly left unital and a strictly right unital concatenation
-operation, while both are strictly associative.
-
-The strict one-sided unitality follows in both cases from the strict right
-unitality of the concatenation operation on the Yoneda identifications,
-following the same computation as for the strictly involutive identity types.
-
-For associativity on the other hand, we must use the strict associativity of the
-Yoneda identity types. We will write out the explicit computation later.
+operation, while both are strictly associative. The strict one-sided unitality
+follows in both cases from the strict right unitality of the concatenation
+operation on the Yoneda identifications, following the same computation as for
+the strictly involutive identity types. For associativity on the other hand, we
+must use the strict associativity of the Yoneda identity types. We will write
+out the explicit computation later.
 
 **Observation.** Since the concatenation operations are strictly associative,
 every string of concatenations containing reflexivities will reduce aside from
@@ -442,7 +441,7 @@ the strictly left unital concatenation operation for the strictly involutive
 identity types
 
 ```text
-  (w , p , q) ∙ʲ (w' , p' , q') := (w' , p' , q' ∙ʸ inv-yoneda-Id p ∙ʸ q)
+  (w , p , q) ∙ʲ (w' , p' , q') := (w' , p' , q' ∙ʸ invʸ p ∙ʸ q)
 ```
 
 ```agda
@@ -452,7 +451,7 @@ module _
 
   infixl 15 _∙ʲ_
   _∙ʲ_ : {x y z : A} → x ＝ʲ y → y ＝ʲ z → x ＝ʲ z
-  (w , p , q) ∙ʲ (w' , p' , q') = (w' , p' , q' ∙ʸ inv-yoneda-Id p ∙ʸ q)
+  (w , p , q) ∙ʲ (w' , p' , q') = (w' , p' , q' ∙ʸ invʸ p ∙ʸ q)
 
   concat-computational-Id : {x y : A} → x ＝ʲ y → (z : A) → y ＝ʲ z → x ＝ʲ z
   concat-computational-Id p z q = p ∙ʲ q
@@ -517,7 +516,7 @@ module _
 
   infixl 15 _∙ᵣʲ_
   _∙ᵣʲ_ : {x y z : A} → x ＝ʲ y → y ＝ʲ z → x ＝ʲ z
-  (w , p , q) ∙ᵣʲ (w' , p' , q') = (w , p ∙ʸ inv-yoneda-Id q' ∙ʸ p' , q)
+  (w , p , q) ∙ᵣʲ (w' , p' , q') = (w , p ∙ʸ invʸ q' ∙ʸ p' , q)
 
   right-strict-concat-computational-Id :
     {x y : A} → x ＝ʲ y → (z : A) → y ＝ʲ z → x ＝ʲ z
@@ -572,11 +571,11 @@ To see that `_∙ʲ_` is strictly associative, we unfold both `(P ∙ʲ Q) ∙ʲ
 ```text
   (P ∙ʲ Q) ∙ʲ R
   ≐ ((u , p , p') ∙ʲ (v , q , q')) ∙ʲ (w , r , r')
-  ≐ ((v , q , (q' ∙ʸ inv p) ∙ʸ p')) ∙ʲ (w , r , r')
-  ≐ (w , r , (r' ∙ʸ inv q) ∙ʸ ((q' ∙ʸ inv p) ∙ʸ p'))
+  ≐ ((v , q , (q' ∙ʸ invʸ p) ∙ʸ p')) ∙ʲ (w , r , r')
+  ≐ (w , r , (r' ∙ʸ invʸ q) ∙ʸ ((q' ∙ʸ invʸ p) ∙ʸ p'))
 
-  ≐ (w , r , (((r' ∙ʸ inv q) ∙ʸ q') ∙ʸ inv p) ∙ʸ p')
-  ≐ (u , p , p') ∙ʲ ((w , r , (r' ∙ʸ inv q) ∙ʸ q'))
+  ≐ (w , r , (((r' ∙ʸ invʸ q) ∙ʸ q') ∙ʸ invʸ p) ∙ʸ p')
+  ≐ (u , p , p') ∙ʲ ((w , r , (r' ∙ʸ invʸ q) ∙ʸ q'))
   ≐ (u , p , p') ∙ʲ ((v , q , q') ∙ʲ (w , r , r'))
   ≐ P ∙ʲ (Q ∙ʲ R).
 ```
@@ -608,35 +607,35 @@ module _
       ( p)
 
   left-inv-concat-computational-Id :
-    (p : x ＝ʲ y) → inv-computational-Id p ∙ʲ p ＝ reflʲ
+    (p : x ＝ʲ y) → invʲ p ∙ʲ p ＝ reflʲ
   left-inv-concat-computational-Id (z , p , q) =
     ind-yoneda-Id
       ( λ _ p →
-        ( inv-computational-Id (z , p , q) ∙ʲ (z , p , q)) ＝
+        ( invʲ (z , p , q) ∙ʲ (z , p , q)) ＝
         ( reflʲ))
       ( eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-yoneda-Id q)))
       ( p)
 
   right-inv-concat-computational-Id :
-    (p : x ＝ʲ y) → p ∙ʲ inv-computational-Id p ＝ reflʲ
+    (p : x ＝ʲ y) → p ∙ʲ invʲ p ＝ reflʲ
   right-inv-concat-computational-Id (z , p , q) =
     ind-yoneda-Id
       ( λ _ q →
-        ( (z , p , q) ∙ʲ inv-computational-Id (z , p , q)) ＝
+        ( (z , p , q) ∙ʲ invʲ (z , p , q)) ＝
         ( reflʲ))
       ( eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-yoneda-Id p)))
       ( q)
 
   distributive-inv-concat-computational-Id :
     (p : x ＝ʲ y) {z : A} (q : y ＝ʲ z) →
-    inv-computational-Id (p ∙ʲ q) ＝
-    inv-computational-Id q ∙ʲ inv-computational-Id p
+    invʲ (p ∙ʲ q) ＝
+    invʲ q ∙ʲ invʲ p
   distributive-inv-concat-computational-Id p =
     ind-computational-Id
       ( λ _ q →
-        inv-computational-Id (p ∙ʲ q) ＝
-        inv-computational-Id q ∙ʲ inv-computational-Id p)
-      ( ap inv-computational-Id (right-unit-concat-computational-Id))
+        invʲ (p ∙ʲ q) ＝
+        invʲ q ∙ʲ invʲ p)
+      ( ap invʲ (right-unit-concat-computational-Id))
 ```
 
 #### The groupoidal laws for the strictly right unital concatenation operation
@@ -666,28 +665,21 @@ module _
   left-unit-right-strict-concat-computational-Id :
     {p : x ＝ʲ y} → reflʲ ∙ᵣʲ p ＝ p
   left-unit-right-strict-concat-computational-Id {z , p , q} =
-    ind-yoneda-Id
-      ( λ _ q → reflʲ ∙ᵣʲ (z , p , q) ＝ (z , p , q))
-      ( refl)
-      ( q)
+    ind-yoneda-Id (λ _ q → reflʲ ∙ᵣʲ (z , p , q) ＝ (z , p , q)) refl q
 
   left-inv-right-strict-concat-computational-Id :
-    (p : x ＝ʲ y) → inv-computational-Id p ∙ᵣʲ p ＝ reflʲ
+    (p : x ＝ʲ y) → invʲ p ∙ᵣʲ p ＝ reflʲ
   left-inv-right-strict-concat-computational-Id (z , p , q) =
     ind-yoneda-Id
-      ( λ _ p →
-        ( inv-computational-Id (z , p , q) ∙ᵣʲ (z , p , q)) ＝
-        ( reflʲ))
+      ( λ _ p → invʲ (z , p , q) ∙ᵣʲ (z , p , q) ＝ reflʲ)
       ( eq-pair-eq-fiber (eq-pair (right-inv-yoneda-Id q) refl))
       ( p)
 
   right-inv-right-strict-concat-computational-Id :
-    (p : x ＝ʲ y) → p ∙ᵣʲ inv-computational-Id p ＝ reflʲ
+    (p : x ＝ʲ y) → p ∙ᵣʲ invʲ p ＝ reflʲ
   right-inv-right-strict-concat-computational-Id (z , p , q) =
     ind-yoneda-Id
-      ( λ _ q →
-        ( (z , p , q) ∙ᵣʲ inv-computational-Id (z , p , q)) ＝
-        ( reflʲ))
+      ( λ _ q → (z , p , q) ∙ᵣʲ invʲ (z , p , q) ＝ reflʲ)
       ( eq-pair-eq-fiber (eq-pair (right-inv-yoneda-Id p) refl))
       ( q)
 
@@ -696,14 +688,10 @@ module _
   where
 
   distributive-inv-right-strict-concat-computational-Id :
-    (p : x ＝ʲ y) {z : A} (q : y ＝ʲ z) →
-    inv-computational-Id (p ∙ᵣʲ q) ＝
-    inv-computational-Id q ∙ᵣʲ inv-computational-Id p
+    (p : x ＝ʲ y) {z : A} (q : y ＝ʲ z) → invʲ (p ∙ᵣʲ q) ＝ invʲ q ∙ᵣʲ invʲ p
   distributive-inv-right-strict-concat-computational-Id p =
     ind-computational-Id
-      ( λ _ q →
-        inv-computational-Id (p ∙ᵣʲ q) ＝
-        inv-computational-Id q ∙ᵣʲ inv-computational-Id p)
+      ( λ _ q → invʲ (p ∙ᵣʲ q) ＝ invʲ q ∙ᵣʲ invʲ p)
       ( inv left-unit-right-strict-concat-computational-Id)
 ```
 
@@ -726,10 +714,10 @@ module _
   ap-computational-Id =
     computational-eq-yoneda-eq ∘ ap-yoneda-Id f ∘ yoneda-eq-computational-eq
 
-  compute-ap-reflʲ :
+  compute-ap-refl-computational-Id :
     {x : A} →
     ap-computational-Id (reflʲ {x = x}) ＝ reflʲ
-  compute-ap-reflʲ = refl
+  compute-ap-refl-computational-Id = refl
 
 module _
   {l1 : Level} {A : UU l1}
@@ -754,9 +742,9 @@ module _
   tr-computational-Id : {x y : A} → x ＝ʲ y → B x → B y
   tr-computational-Id = tr B ∘ eq-computational-eq
 
-  compute-tr-reflʲ :
+  compute-tr-refl-computational-Id :
     {x : A} → tr-computational-Id (reflʲ {x = x}) ＝ id
-  compute-tr-reflʲ = refl
+  compute-tr-refl-computational-Id = refl
 ```
 
 ### Function extensionality with respect to computational identifications
diff --git a/src/foundation/strictly-involutive-identity-types.lagda.md b/src/foundation/strictly-involutive-identity-types.lagda.md
index 4038f825c2..0484a7fb0a 100644
--- a/src/foundation/strictly-involutive-identity-types.lagda.md
+++ b/src/foundation/strictly-involutive-identity-types.lagda.md
@@ -44,15 +44,15 @@ whose elements we call
 family is [equivalent](foundation-core.equivalences.md) to the standard identity
 types, but satisfies the strict laws
 
-- `inv (inv p) ≐ p`
-- `inv reflⁱ ≐ reflⁱ`
+- `invⁱ (invⁱ p) ≐ p`
+- `invⁱ reflⁱ ≐ reflⁱ`
 
 where we use a superscript `i` to distinguish the strictly involutive identity
 type from the standard identity type.
 
 In addition, we maintain the following strict laws
 
-- `inv reflⁱ ≐ reflⁱ`
+- `invⁱ reflⁱ ≐ reflⁱ`
 - `reflⁱ ∙ p ≐ p` or `p ∙ reflⁱ ≐ p`
 - `ind-Idⁱ B f reflⁱ ≐ f reflⁱ`
 
@@ -248,24 +248,21 @@ groupoidal structure on types.
 We have an inversion operation on `involutive-Id` defined by swapping the
 position of the identifications. This operation satisfies the strict laws
 
-- `inv (inv p) ≐ p`, and
-- `inv reflⁱ ≐ reflⁱ`.
+- `invⁱ (invⁱ p) ≐ p`, and
+- `invⁱ reflⁱ ≐ reflⁱ`.
 
 ```agda
 module _
   {l : Level} {A : UU l}
   where
 
-  inv-involutive-Id : {x y : A} → x ＝ⁱ y → y ＝ⁱ x
-  inv-involutive-Id (z , p , q) = (z , q , p)
+  invⁱ : {x y : A} → x ＝ⁱ y → y ＝ⁱ x
+  invⁱ (z , p , q) = (z , q , p)
 
-  compute-inv-involutive-Id-refl :
-    {x : A} →
-    inv-involutive-Id (reflⁱ {x = x}) ＝ reflⁱ
-  compute-inv-involutive-Id-refl = refl
+  compute-refl-inv-involutive-Id : {x : A} → invⁱ (reflⁱ {x = x}) ＝ reflⁱ
+  compute-refl-inv-involutive-Id = refl
 
-  inv-inv-involutive-Id :
-    {x y : A} (p : x ＝ⁱ y) → inv-involutive-Id (inv-involutive-Id p) ＝ p
+  inv-inv-involutive-Id : {x y : A} (p : x ＝ⁱ y) → invⁱ (invⁱ p) ＝ p
   inv-inv-involutive-Id p = refl
 ```
 
@@ -279,12 +276,12 @@ module _
 
   preserves-inv-involutive-eq-eq :
     {x y : A} (p : x ＝ y) →
-    involutive-eq-eq (inv p) ＝ inv-involutive-Id (involutive-eq-eq p)
+    involutive-eq-eq (inv p) ＝ invⁱ (involutive-eq-eq p)
   preserves-inv-involutive-eq-eq refl = refl
 
   preserves-inv-eq-involutive-eq :
     {x y : A} (p : x ＝ⁱ y) →
-    eq-involutive-eq (inv-involutive-Id p) ＝ inv (eq-involutive-eq p)
+    eq-involutive-eq (invⁱ p) ＝ inv (eq-involutive-eq p)
   preserves-inv-eq-involutive-eq (z , p , q) =
     ap (inv p ∙_) (inv (inv-inv q)) ∙ inv (distributive-inv-concat (inv q) p)
 ```
@@ -439,8 +436,7 @@ module _
   where
 
   assoc-involutive-Id :
-    (p : x ＝ⁱ y) (q : y ＝ⁱ z) (r : z ＝ⁱ w) →
-    ((p ∙ⁱ q) ∙ⁱ r) ＝ (p ∙ⁱ (q ∙ⁱ r))
+    (p : x ＝ⁱ y) (q : y ＝ⁱ z) (r : z ＝ⁱ w) → (p ∙ⁱ q) ∙ⁱ r ＝ p ∙ⁱ (q ∙ⁱ r)
   assoc-involutive-Id (_ , p , q) (_ , p' , q') (_ , p'' , q'') =
     eq-pair-eq-fiber
       ( eq-pair-eq-fiber
@@ -470,18 +466,17 @@ module _
     eq-pair-eq-fiber (eq-pair-eq-fiber left-unit-right-strict-concat)
 
   left-inv-involutive-Id :
-    (p : x ＝ⁱ y) → inv-involutive-Id p ∙ⁱ p ＝ reflⁱ
+    (p : x ＝ⁱ y) → invⁱ p ∙ⁱ p ＝ reflⁱ
   left-inv-involutive-Id (.y , refl , q) =
     eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-right-strict-concat q))
 
   right-inv-involutive-Id :
-    (p : x ＝ⁱ y) → p ∙ⁱ inv-involutive-Id p ＝ reflⁱ
+    (p : x ＝ⁱ y) → p ∙ⁱ invⁱ p ＝ reflⁱ
   right-inv-involutive-Id (.x , p , refl) =
     eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-right-strict-concat p))
 
   distributive-inv-concat-involutive-Id :
-    (p : x ＝ⁱ y) {z : A} (q : y ＝ⁱ z) →
-    inv-involutive-Id (p ∙ⁱ q) ＝ inv-involutive-Id q ∙ⁱ inv-involutive-Id p
+    (p : x ＝ⁱ y) {z : A} (q : y ＝ⁱ z) → invⁱ (p ∙ⁱ q) ＝ invⁱ q ∙ⁱ invⁱ p
   distributive-inv-concat-involutive-Id (.y , refl , q') (.y , p' , refl) =
     eq-pair-eq-fiber
       ( eq-pair
@@ -497,8 +492,7 @@ module _
   where
 
   assoc-right-strict-concat-involutive-Id :
-    (p : x ＝ⁱ y) (q : y ＝ⁱ z) (r : z ＝ⁱ w) →
-    ((p ∙ᵣⁱ q) ∙ᵣⁱ r) ＝ (p ∙ᵣⁱ (q ∙ᵣⁱ r))
+    (p : x ＝ⁱ y) (q : y ＝ⁱ z) (r : z ＝ⁱ w) → (p ∙ᵣⁱ q) ∙ᵣⁱ r ＝ p ∙ᵣⁱ (q ∙ᵣⁱ r)
   assoc-right-strict-concat-involutive-Id
     ( _ , p , q) (_ , p' , q') (_ , p'' , q'') =
     eq-pair-eq-fiber
@@ -524,18 +518,18 @@ module _
   right-unit-right-strict-concat-involutive-Id = refl
 
   left-inv-right-strict-concat-involutive-Id :
-    (p : x ＝ⁱ y) → inv-involutive-Id p ∙ᵣⁱ p ＝ reflⁱ
+    (p : x ＝ⁱ y) → invⁱ p ∙ᵣⁱ p ＝ reflⁱ
   left-inv-right-strict-concat-involutive-Id (.y , refl , q) =
     eq-pair-eq-fiber (eq-pair (right-inv-right-strict-concat q) refl)
 
   right-inv-right-strict-concat-involutive-Id :
-    (p : x ＝ⁱ y) → p ∙ᵣⁱ inv-involutive-Id p ＝ reflⁱ
+    (p : x ＝ⁱ y) → p ∙ᵣⁱ invⁱ p ＝ reflⁱ
   right-inv-right-strict-concat-involutive-Id (.x , p , refl) =
     eq-pair-eq-fiber (eq-pair (right-inv-right-strict-concat p) refl)
 
   distributive-inv-right-strict-concat-involutive-Id :
     (p : x ＝ⁱ y) {z : A} (q : y ＝ⁱ z) →
-    inv-involutive-Id (p ∙ᵣⁱ q) ＝ inv-involutive-Id q ∙ᵣⁱ inv-involutive-Id p
+    invⁱ (p ∙ᵣⁱ q) ＝ invⁱ q ∙ᵣⁱ invⁱ p
   distributive-inv-right-strict-concat-involutive-Id
     ( .y , refl , q) (.y , p' , refl) =
     eq-pair-eq-fiber
diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 2331817ce2..9a139f3a84 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -7,8 +7,8 @@ module foundation.yoneda-identity-types where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
 open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.multivariable-homotopies
@@ -62,7 +62,7 @@ concretely, the reflexivity is given by the identity function, and path
 concatenation is given by function composition.
 
 In addition to these strictness laws, we can make the type satisfy the strict
-law `inv reflʸ ≐ reflʸ`. Moreover, while the induction principle of the Yoneda
+law `invʸ reflʸ ≐ reflʸ`. Moreover, while the induction principle of the Yoneda
 identity types does not in general satisfy the computation rule strictly, we can
 define its recursion principle such that does.
 
@@ -427,7 +427,7 @@ concatenation operation on the underlying identity type respectively. In
 contrast to the latter, the former enjoys the computational property
 
 ```text
-  inv reflʸ ≐ reflʸ,
+  invʸ reflʸ ≐ reflʸ,
 ```
 
 hence it will be preferred going forward.
@@ -439,17 +439,15 @@ module _
   {l : Level} {A : UU l}
   where
 
-  inv-yoneda-Id : {x y : A} → x ＝ʸ y → y ＝ʸ x
-  inv-yoneda-Id {x} f z p = p ∙ᵣ inv (f x refl)
+  invʸ : {x y : A} → x ＝ʸ y → y ＝ʸ x
+  invʸ {x} f z p = p ∙ᵣ inv (f x refl)
 
-  compute-inv-yoneda-Id-refl :
-    {x : A} →
-    inv-yoneda-Id (reflʸ {x = x}) ＝ reflʸ
-  compute-inv-yoneda-Id-refl = refl
+  compute-inv-refl-yoneda-Id :
+    {x : A} → invʸ (reflʸ {x = x}) ＝ reflʸ
+  compute-inv-refl-yoneda-Id = refl
 
   inv-inv-yoneda-Id :
-    {x y : A} (f : x ＝ʸ y) →
-    inv-yoneda-Id (inv-yoneda-Id f) ＝ f
+    {x y : A} (f : x ＝ʸ y) → invʸ (invʸ f) ＝ f
   inv-inv-yoneda-Id {x} f =
     eq-multivariable-htpy 2
       ( λ _ p →
@@ -468,20 +466,17 @@ module _
   where
 
   preserves-inv-yoneda-eq-eq' :
-    {x y : A} (p : x ＝ y) →
-    yoneda-eq-eq (inv p) ＝ inv-yoneda-Id (yoneda-eq-eq' p)
+    {x y : A} (p : x ＝ y) → yoneda-eq-eq (inv p) ＝ invʸ (yoneda-eq-eq' p)
   preserves-inv-yoneda-eq-eq' p = refl
 
   preserves-inv-yoneda-eq-eq :
-    {x y : A} (p : x ＝ y) →
-    yoneda-eq-eq (inv p) ＝ inv-yoneda-Id (yoneda-eq-eq p)
+    {x y : A} (p : x ＝ y) → yoneda-eq-eq (inv p) ＝ invʸ (yoneda-eq-eq p)
   preserves-inv-yoneda-eq-eq p =
     eq-multivariable-htpy 2
       ( λ _ q → ap (λ r → q ∙ᵣ inv r) (inv left-unit-right-strict-concat))
 
   preserves-inv-eq-yoneda-eq :
-    {x y : A} (f : x ＝ʸ y) →
-    eq-yoneda-eq (inv-yoneda-Id f) ＝ inv (eq-yoneda-eq f)
+    {x y : A} (f : x ＝ʸ y) → eq-yoneda-eq (invʸ f) ＝ inv (eq-yoneda-eq f)
   preserves-inv-eq-yoneda-eq f = left-unit-right-strict-concat
 ```
 
@@ -583,6 +578,8 @@ module _
 
 ### The groupoidal laws for the Yoneda identity types
 
+As we may now observe, associativity and the unit laws holds by `refl`.
+
 ```agda
 module _
   {l : Level} {A : UU l} {x y : A}
@@ -600,9 +597,14 @@ module _
   right-unit-yoneda-Id :
     {f : x ＝ʸ y} → f ∙ʸ reflʸ ＝ f
   right-unit-yoneda-Id = refl
+```
 
+In addition, we show a range of basic algebraic laws for the Yoneda identity
+types.
+
+```agda
   left-inv-yoneda-Id :
-    (f : x ＝ʸ y) → inv-yoneda-Id f ∙ʸ f ＝ reflʸ
+    (f : x ＝ʸ y) → invʸ f ∙ʸ f ＝ reflʸ
   left-inv-yoneda-Id f =
     eq-multivariable-htpy 2
       ( λ _ p →
@@ -618,7 +620,7 @@ module _
         ( ap (p ∙_) (compute-inv-Id-yoneda-Id f) ∙ right-unit))
 
   right-inv-yoneda-Id :
-    (f : x ＝ʸ y) → f ∙ʸ inv-yoneda-Id f ＝ reflʸ
+    (f : x ＝ʸ y) → f ∙ʸ invʸ f ＝ reflʸ
   right-inv-yoneda-Id f =
     eq-multivariable-htpy 2
       ( λ _ p →
@@ -642,7 +644,7 @@ module _
 
   distributive-inv-concat-yoneda-Id :
     (f : x ＝ʸ y) {z : A} (g : y ＝ʸ z) →
-    inv-yoneda-Id (f ∙ʸ g) ＝ inv-yoneda-Id g ∙ʸ inv-yoneda-Id f
+    invʸ (f ∙ʸ g) ＝ invʸ g ∙ʸ invʸ f
   distributive-inv-concat-yoneda-Id f g =
     eq-multivariable-htpy 2
       ( λ _ p →
@@ -689,16 +691,14 @@ module _
   ap-yoneda-Id : {x y : A} → x ＝ʸ y → f x ＝ʸ f y
   ap-yoneda-Id = yoneda-eq-eq ∘ eq-ap-yoneda-Id
 
-  compute-ap-reflʸ :
-    {x : A} → ap-yoneda-Id (reflʸ {x = x}) ＝ reflʸ
+  compute-ap-reflʸ : {x : A} → ap-yoneda-Id (reflʸ {x = x}) ＝ reflʸ
   compute-ap-reflʸ = refl
 
 module _
   {l1 : Level} {A : UU l1}
   where
 
-  compute-ap-id-yoneda-Id :
-    {x y : A} (p : x ＝ʸ y) → ap-yoneda-Id id p ＝ p
+  compute-ap-id-yoneda-Id : {x y : A} (p : x ＝ʸ y) → ap-yoneda-Id id p ＝ p
   compute-ap-id-yoneda-Id {x} p =
     eq-multivariable-htpy 2
       ( λ _ q →
@@ -708,6 +708,24 @@ module _
 
 ### Action of binary functions on Yoneda identifications
 
+Using one of the two sides in the Gray interchange diagram
+
+```text
+                         ap (f x) q
+                 f x y -------------- f x y'
+                   |                    |
+                   |                    |
+  ap (r ↦ f r y) p |                    | ap (r ↦ f r y') p
+                   |                    |
+                   |                    |
+                 f x' y ------------- f x' y'
+                         ap (f x') q
+```
+
+and the fact that the concatenation operation on Yoneda identifications is
+two-sided strictly unital, we obtain an action of binary functions on Yoneda
+identifications that computes on both inputs.
+
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → B → C)
@@ -717,6 +735,16 @@ module _
     {x x' : A} (p : x ＝ʸ x') {y y' : B} (q : y ＝ʸ y') → f x y ＝ʸ f x' y'
   ap-binary-yoneda-Id {x} {x'} p {y} {y'} q =
     ap-yoneda-Id (λ z → f z y) p ∙ʸ ap-yoneda-Id (f x') q
+
+  left-unit-ap-binary-Id :
+    {x : A} {y y' : B} (q : y ＝ʸ y') →
+    ap-binary-yoneda-Id reflʸ q ＝ ap-yoneda-Id (f x) q
+  left-unit-ap-binary-Id q = refl
+
+  right-unit-ap-binary-Id :
+    {x x' : A} (p : x ＝ʸ x') {y : B} →
+    ap-binary-yoneda-Id p reflʸ ＝ ap-yoneda-Id (λ z → f z y) p
+  right-unit-ap-binary-Id p = refl
 ```
 
 ### Transport along Yoneda identifications
@@ -729,12 +757,11 @@ module _
   tr-yoneda-Id : {x y : A} → x ＝ʸ y → B x → B y
   tr-yoneda-Id = tr B ∘ eq-yoneda-eq
 
-  compute-tr-reflʸ :
-    {x : A} → tr-yoneda-Id (reflʸ {x = x}) ＝ id
+  compute-tr-reflʸ : {x : A} → tr-yoneda-Id (reflʸ {x = x}) ＝ id
   compute-tr-reflʸ = refl
 ```
 
-### Function extensionality with respect to Yoneda identifications
+### Standard function extensionality with respect to Yoneda identifications
 
 ```agda
 module _
@@ -757,7 +784,7 @@ module _
   funext-yoneda-Id = is-equiv-map-equiv equiv-htpy-yoneda-eq
 ```
 
-### Univalence with respect to Yoneda identifications
+### Standard univalence with respect to Yoneda identifications
 
 ```agda
 module _
@@ -786,7 +813,7 @@ module _
   is-equiv-yoneda-eq-equiv = is-equiv-map-equiv equiv-yoneda-eq-equiv
 ```
 
-### Horizontal concatenation of yoneda identifications
+### Horizontal concatenation of Yoneda identifications
 
 ```agda
 module _
@@ -797,16 +824,48 @@ module _
     {p q : x ＝ʸ y} → p ＝ʸ q → {u v : y ＝ʸ z} → u ＝ʸ v → p ∙ʸ u ＝ʸ q ∙ʸ v
   horizontal-concat-yoneda-Id² α β = ap-binary-yoneda-Id (_∙ʸ_) α β
 
-  left-unit-horizontal-concat-yoneda-Id² :
+  compute-left-horizontal-concat-yoneda-Id² :
     {p : x ＝ʸ y} {u v : y ＝ʸ z} (β : u ＝ʸ v) →
     horizontal-concat-yoneda-Id² reflʸ β ＝ ap-yoneda-Id (p ∙ʸ_) β
-  left-unit-horizontal-concat-yoneda-Id² β = refl
+  compute-left-horizontal-concat-yoneda-Id² β = refl
 
-  right-unit-horizontal-concat-yoneda-Id² :
+  compute-right-horizontal-concat-yoneda-Id² :
     {p q : x ＝ʸ y} (α : p ＝ʸ q) {u : y ＝ʸ z} →
     horizontal-concat-yoneda-Id² α (reflʸ {x = u}) ＝ ap-yoneda-Id (_∙ʸ u) α
-  right-unit-horizontal-concat-yoneda-Id² α = refl
+  compute-right-horizontal-concat-yoneda-Id² α = refl
+
+module _
+  {l : Level} {A : UU l} {x y : A}
+  where
+
+  left-unit-horizontal-concat-yoneda-Id² :
+    {p q : x ＝ʸ y} (α : p ＝ʸ q) →
+    horizontal-concat-yoneda-Id² reflʸ α ＝ α
+  left-unit-horizontal-concat-yoneda-Id² = compute-ap-id-yoneda-Id
+
+  right-unit-horizontal-concat-yoneda-Id² :
+    {p q : x ＝ʸ y} (α : p ＝ʸ q) →
+    horizontal-concat-yoneda-Id² α (reflʸ {x = reflʸ}) ＝ α
+  right-unit-horizontal-concat-yoneda-Id² = compute-ap-id-yoneda-Id
+```
+
+Since concatenation on Yoneda identifications is strictly associative, the
+composites
+
+```text
+  horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² α β) γ
+```
+
+and
+
+```text
+  horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ)
+```
+
+live in the same type. Hence, we can pose the question of whether the horizontal
+concatenation operation is associative, which it is weakly:
 
+```agda
 module _
   {l : Level} {A : UU l} {x y z w : A}
   where
@@ -819,14 +878,36 @@ module _
     horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ)
   assoc-horizontal-concat-yoneda-Id² {p} α {q} β γ =
     ind-yoneda-Id
-      ( λ _ α → horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² α β) γ ＝ horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ))
-        (ind-yoneda-Id
-          ( λ _ β → horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² reflʸ β) γ ＝ horizontal-concat-yoneda-Id² reflʸ (horizontal-concat-yoneda-Id² β γ))
-          ( ind-yoneda-Id (λ _ γ → horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² (reflʸ {x = p}) (reflʸ {x = q})) γ ＝ horizontal-concat-yoneda-Id² (reflʸ {x = p}) (horizontal-concat-yoneda-Id² (reflʸ {x = q}) γ)) refl γ)
-          β) α
-```
-
-### Vertical concatenation of yoneda identifications
+      ( λ _ α →
+        ( horizontal-concat-yoneda-Id²
+          ( horizontal-concat-yoneda-Id² α β)
+          ( γ)) ＝
+        ( horizontal-concat-yoneda-Id²
+          ( α)
+          ( horizontal-concat-yoneda-Id² β γ)))
+      ( ind-yoneda-Id
+        ( λ _ β →
+          ( horizontal-concat-yoneda-Id²
+            ( horizontal-concat-yoneda-Id² reflʸ β)
+            ( γ)) ＝
+          ( horizontal-concat-yoneda-Id²
+            ( reflʸ)
+            ( horizontal-concat-yoneda-Id² β γ)))
+        ( ind-yoneda-Id
+          ( λ _ γ →
+            ( horizontal-concat-yoneda-Id²
+              ( horizontal-concat-yoneda-Id² (reflʸ {x = p}) (reflʸ {x = q}))
+              ( γ)) ＝
+            ( horizontal-concat-yoneda-Id²
+              ( reflʸ {x = p})
+              ( horizontal-concat-yoneda-Id² (reflʸ {x = q}) γ)))
+          ( refl)
+          ( γ))
+        ( β))
+      ( α)
+```
+
+### Vertical concatenation of Yoneda identifications
 
 ```agda
 module _

From 7ff9b407502e349d6da781b1ee0168c69f2f0912 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 9 Feb 2024 11:46:41 +0100
Subject: [PATCH 03/14] make library typecheck with new definition of
 `ap-binary`

---
 src/foundation/path-algebra.lagda.md          |  24 +--
 .../double-loop-spaces.lagda.md               |   4 +-
 .../eckmann-hilton-argument.lagda.md          | 198 +++++++++---------
 .../triple-loop-spaces.lagda.md               |   4 +-
 4 files changed, 110 insertions(+), 120 deletions(-)

diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
index 36ca00877d..1f3a4b8a7e 100644
--- a/src/foundation/path-algebra.lagda.md
+++ b/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
 
-left-unit-law-horizontal-concat-Id² :
+compute-left-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 γ
-left-unit-law-horizontal-concat-Id² = left-unit-ap-binary (_∙_)
+compute-left-horizontal-concat-Id² = left-unit-ap-binary (_∙_)
 
-right-unit-law-horizontal-concat-Id² :
+compute-right-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
-right-unit-law-horizontal-concat-Id² = right-unit-ap-binary (_∙_)
+compute-right-horizontal-concat-Id² = right-unit-ap-binary (_∙_)
 ```
 
 Horizontal concatenation satisfies an additional "2-dimensional" unit law (on
@@ -202,7 +202,7 @@ module _
   nat-sq-right-unit-Id² =
     ( ( horizontal-concat-Id² refl (inv (ap-id α))) ∙
       ( nat-htpy htpy-right-unit α)) ∙
-    ( horizontal-concat-Id² (inv (right-unit-law-horizontal-concat-Id² α)) refl)
+    ( horizontal-concat-Id² (inv (compute-right-horizontal-concat-Id² α)) refl)
 
   nat-sq-left-unit-Id² :
     coherence-square-identifications
@@ -212,7 +212,7 @@ module _
       ( α)
   nat-sq-left-unit-Id² =
     ( ( (inv (ap-id α) ∙ (nat-htpy htpy-left-unit α)) ∙ right-unit) ∙
-      ( inv (left-unit-law-horizontal-concat-Id² α))) ∙
+      ( inv (compute-left-horizontal-concat-Id² α))) ∙
     ( inv right-unit)
 ```
 
@@ -287,8 +287,8 @@ interchange-Id² refl refl refl refl = refl
 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 ∙ right-unit-law-horizontal-concat-Id² α)) ＝
-  ( ( right-unit-law-horizontal-concat-Id² (α ∙ refl)) ∙
+    ( right-unit ∙ compute-right-horizontal-concat-Id² α)) ＝
+  ( ( compute-right-horizontal-concat-Id² (α ∙ refl)) ∙
     ( ap (λ s → right-whisker-concat s u) right-unit))
 unit-law-α-interchange-Id² refl u = refl
 
@@ -300,8 +300,8 @@ unit-law-β-interchange-Id² refl u = 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 ∙ left-unit-law-horizontal-concat-Id² γ)) ＝
-  ( ( left-unit-law-horizontal-concat-Id² (γ ∙ refl)) ∙
+    ( right-unit ∙ compute-left-horizontal-concat-Id² γ)) ＝
+  ( ( compute-left-horizontal-concat-Id² (γ ∙ refl)) ∙
     ( ap (left-whisker-concat p) right-unit))
 unit-law-γ-interchange-Id² p refl = refl
 
@@ -373,13 +373,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³ {τ = τ} = left-unit-law-horizontal-concat-Id² τ
+left-unit-law-y-concat-Id³ {τ = τ} = compute-left-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³ {σ = σ} = right-unit-law-horizontal-concat-Id² σ
+right-unit-law-y-concat-Id³ {σ = σ} = compute-right-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}
diff --git a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
index a756011d87..a32fc552af 100644
--- a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
@@ -83,7 +83,7 @@ module _
     {a : A} {α : type-Ω² a} →
     Id (horizontal-concat-Ω² refl-Ω² α) α
   left-unit-law-horizontal-concat-Ω² {α = α} =
-    ( left-unit-law-horizontal-concat-Id² α) ∙ (ap-id α)
+    ( compute-left-horizontal-concat-Id² α) ∙ (ap-id α)
 
   naturality-right-unit :
     {x y : A} {p q : Id x y} (α : Id p q) →
@@ -103,7 +103,7 @@ module _
     {a : A} {α : type-Ω² a} →
     Id (horizontal-concat-Ω² α refl-Ω²) α
   right-unit-law-horizontal-concat-Ω² {α = α} =
-    ( right-unit-law-horizontal-concat-Id² α) ∙ (naturality-right-unit-Ω² α)
+    ( compute-right-horizontal-concat-Id² α) ∙ (naturality-right-unit-Ω² α)
 
   left-unit-law-left-whisker-Ω² :
     {a : A} (α : type-Ω² a) →
diff --git a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
index a064546334..fd4281dffe 100644
--- a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
+++ b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
@@ -61,41 +61,41 @@ is a group homomorphism of
 in each variable.
 
 ```agda
-outer-eckmann-hilton-interchange-connection-Ω² :
-  {l : Level} {A : UU l} {a : A} (α δ : type-Ω² a) →
-  Id (horizontal-concat-Ω² α δ) (vertical-concat-Ω² α δ)
-outer-eckmann-hilton-interchange-connection-Ω² α δ =
-  ( z-concat-Id³ (inv right-unit) (inv left-unit)) ∙
-  ( ( interchange-Ω² α refl refl δ) ∙
-    ( y-concat-Id³
-      ( right-unit-law-horizontal-concat-Ω² {α = α})
-      ( left-unit-law-horizontal-concat-Ω² {α = δ})))
-
-inner-eckmann-hilton-interchange-connection-Ω² :
-  {l : Level} {A : UU l} {a : A} (β γ : type-Ω² a) →
-  Id ( horizontal-concat-Ω² β γ) (vertical-concat-Ω² γ β)
-inner-eckmann-hilton-interchange-connection-Ω² β γ =
-  ( z-concat-Id³ (inv left-unit) (inv right-unit)) ∙
-  ( ( interchange-Ω² refl β γ refl) ∙
-    ( y-concat-Id³
-      ( left-unit-law-horizontal-concat-Ω² {α = γ})
-      ( right-unit-law-horizontal-concat-Ω² {α = β})))
-
-eckmann-hilton-interchange-Ω² :
-  {l : Level} {A : UU l} {a : A} (α β : type-Ω² a) →
-  Id (α ∙ β) (β ∙ α)
-eckmann-hilton-interchange-Ω² α β =
-  ( inv (outer-eckmann-hilton-interchange-connection-Ω² α β)) ∙
-  ( inner-eckmann-hilton-interchange-connection-Ω² α β)
-
-interchange-concat-Ω² :
-  {l : Level} {A : UU l} {a : A} (α β γ δ : type-Ω² a) →
-  ((α ∙ β) ∙ (γ ∙ δ)) ＝ ((α ∙ γ) ∙ (β ∙ δ))
-interchange-concat-Ω² =
-  interchange-law-commutative-and-associative
-    ( _∙_)
-    ( eckmann-hilton-interchange-Ω²)
-    ( assoc)
+module _
+  {l : Level} {A : UU l} {a : A}
+  where
+
+  outer-eckmann-hilton-interchange-connection-Ω² :
+    (α δ : type-Ω² a) →
+    horizontal-concat-Ω² α δ ＝ vertical-concat-Ω² α δ
+  outer-eckmann-hilton-interchange-connection-Ω² α δ =
+    ( z-concat-Id³ {α = α} {γ = δ} (inv right-unit) (inv left-unit)) ∙
+    ( ( interchange-Ω² α refl refl δ) ∙
+      ( y-concat-Id³ {β = α} {δ = δ}
+        ( right-unit-law-horizontal-concat-Ω² {α = α})
+        ( left-unit-law-horizontal-concat-Ω² {α = δ})))
+
+  inner-eckmann-hilton-interchange-connection-Ω² :
+    (β γ : type-Ω² a) → horizontal-concat-Ω² β γ ＝ vertical-concat-Ω² γ β
+  inner-eckmann-hilton-interchange-connection-Ω² β γ =
+    ( z-concat-Id³ {α = β} {β} {γ} (inv left-unit) (inv right-unit)) ∙
+    ( ( interchange-Ω² refl β γ refl) ∙
+      ( y-concat-Id³ {β = γ} {δ = β}
+        ( left-unit-law-horizontal-concat-Ω² {α = γ})
+        ( right-unit-law-horizontal-concat-Ω² {α = β})))
+
+  eckmann-hilton-interchange-Ω² : (α β : type-Ω² a) → α ∙ β ＝ β ∙ α
+  eckmann-hilton-interchange-Ω² α β =
+    ( inv (outer-eckmann-hilton-interchange-connection-Ω² α β)) ∙
+    ( inner-eckmann-hilton-interchange-connection-Ω² α β)
+
+  interchange-concat-Ω² :
+    (α β γ δ : type-Ω² a) → (α ∙ β) ∙ (γ ∙ δ) ＝ (α ∙ γ) ∙ (β ∙ δ)
+  interchange-concat-Ω² =
+    interchange-law-commutative-and-associative
+      ( _∙_)
+      ( eckmann-hilton-interchange-Ω²)
+      ( assoc)
 ```
 
 ### Constructing the Eckmann-Hilton identification using the naturality condition of the operation of whiskering a fixed 2-path by a 1-path
@@ -170,21 +170,23 @@ module _
 
   eckmann-hilton-Ω² :
     (α β : type-Ω² (point-Pointed-Type A)) → α ∙ β ＝ β ∙ α
-  eckmann-hilton-Ω² α β = equational-reasoning_
+  eckmann-hilton-Ω² α β =
+    equational-reasoning
     (α ∙ β) ＝
-    ( left-whisker-concat refl α) ∙
-      ( right-whisker-concat β refl)
-    by ( inv
-      ( horizontal-concat-Id²
-        ( left-unit-law-left-whisker-Ω² α)
-        ( right-unit-law-right-whisker-Ω² β)))
+    ( left-whisker-concat refl α ∙ right-whisker-concat β refl)
+    by
+      ( inv
+        ( horizontal-concat-Id²
+          ( left-unit-law-left-whisker-Ω² α)
+          ( right-unit-law-right-whisker-Ω² β)))
     ＝ ( right-whisker-concat β refl) ∙
       ( left-whisker-concat refl α)
     by ( commutative-left-whisker-right-whisker-concat α β)
     ＝ β ∙ α
-    by ( horizontal-concat-Id²
-      ( right-unit-law-right-whisker-Ω² β)
-      ( left-unit-law-left-whisker-Ω² α))
+    by
+      ( horizontal-concat-Id²
+        ( right-unit-law-right-whisker-Ω² β)
+        ( left-unit-law-left-whisker-Ω² α))
 ```
 
 #### Using right whiskering
@@ -209,21 +211,22 @@ module _
 
   eckmann-hilton-inverse-Ω² :
     (α β : type-Ω² (point-Pointed-Type A)) → α ∙ β ＝ β ∙ α
-  eckmann-hilton-inverse-Ω² α β = equational-reasoning_
+  eckmann-hilton-inverse-Ω² α β =
+    equational-reasoning
     (α ∙ β)
-    ＝ ( right-whisker-concat α refl) ∙
-      ( left-whisker-concat refl β)
-    by ( inv
-      ( horizontal-concat-Id²
-        ( right-unit-law-right-whisker-Ω² α)
-        ( left-unit-law-left-whisker-Ω² β)))
-    ＝ ( left-whisker-concat refl β) ∙
-      ( right-whisker-concat α refl)
+    ＝ (right-whisker-concat α refl ∙ left-whisker-concat refl β)
+    by
+      ( inv
+        ( horizontal-concat-Id²
+          ( right-unit-law-right-whisker-Ω² α)
+          ( left-unit-law-left-whisker-Ω² β)))
+    ＝ (left-whisker-concat refl β ∙ right-whisker-concat α refl)
     by commutative-right-whisker-left-whisker-concat α β
     ＝ β ∙ α
-    by ( horizontal-concat-Id²
-        ( left-unit-law-left-whisker-Ω² β))
-        ( right-unit-law-right-whisker-Ω² α)
+    by
+      ( horizontal-concat-Id²
+        ( left-unit-law-left-whisker-Ω² β)
+        ( right-unit-law-right-whisker-Ω² α))
 ```
 
 We now prove that this Eckmann-Hilton identification "undoes" the previously
@@ -249,42 +252,36 @@ module _
   eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² :
     (α β : type-Ω² (point-Pointed-Type A)) →
     inv (eckmann-hilton-inverse-Ω² β α) ＝ (eckmann-hilton-Ω² α β)
-  eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² α β = equational-reasoning_
+  eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² α β =
+    equational-reasoning
     ( inv (eckmann-hilton-inverse-Ω² β α))
-    ＝ concat
-      ( inv
-        ( horizontal-concat-Id²
-          ( left-unit-law-left-whisker-Ω² α)
-            ( right-unit-law-right-whisker-Ω² β)))
-      ( _)
-      ( inv
-        ( concat
-          ( inv
-            ( horizontal-concat-Id²
-              ( right-unit-law-right-whisker-Ω² β)
-              ( left-unit-law-left-whisker-Ω² α)))
-          ( _)
-          ( commutative-right-whisker-left-whisker-concat β α)))
-    by distributive-inv-concat
-      ( concat
+    ＝
         ( inv
+          ( horizontal-concat-Id²
+            ( left-unit-law-left-whisker-Ω² α)
+              ( right-unit-law-right-whisker-Ω² β))) ∙
+        ( inv
+          (
+            ( inv
+              ( horizontal-concat-Id²
+                ( right-unit-law-right-whisker-Ω² β)
+                ( left-unit-law-left-whisker-Ω² α))) ∙
+            ( commutative-right-whisker-left-whisker-concat β α)))
+    by distributive-inv-concat
+      ( ( inv
           ( horizontal-concat-Id²
             ( right-unit-law-right-whisker-Ω² β)
-            ( left-unit-law-left-whisker-Ω² α)))
-        ( _)
+            ( left-unit-law-left-whisker-Ω² α))) ∙
         ( commutative-right-whisker-left-whisker-concat β α))
       ( horizontal-concat-Id²
         ( left-unit-law-left-whisker-Ω² α)
         ( right-unit-law-right-whisker-Ω² β))
-    ＝ concat
+    ＝
       ( inv
         ( horizontal-concat-Id²
           ( left-unit-law-left-whisker-Ω² α)
-            ( right-unit-law-right-whisker-Ω² β)))
-      ( _)
-      ( concat
-        ( inv (commutative-right-whisker-left-whisker-concat β α))
-        ( _)
+            ( right-unit-law-right-whisker-Ω² β))) ∙
+      ( ( inv (commutative-right-whisker-left-whisker-concat β α)) ∙
         ( inv
           ( inv
             ( horizontal-concat-Id²
@@ -301,15 +298,12 @@ module _
             ( right-unit-law-right-whisker-Ω² β)
             ( left-unit-law-left-whisker-Ω² α)))
         ( commutative-right-whisker-left-whisker-concat β α))
-    ＝ concat
+    ＝
       ( inv
         ( horizontal-concat-Id²
           ( left-unit-law-left-whisker-Ω² α)
-            ( right-unit-law-right-whisker-Ω² β)))
-      ( _)
-      ( concat
-        ( commutative-left-whisker-right-whisker-concat α β)
-        ( _)
+            ( right-unit-law-right-whisker-Ω² β))) ∙
+      ( ( commutative-left-whisker-right-whisker-concat α β) ∙
         ( horizontal-concat-Id²
           ( right-unit-law-right-whisker-Ω² β)
           ( left-unit-law-left-whisker-Ω² α)))
@@ -346,15 +340,13 @@ module _
   {l : Level} {A : UU l} {a : A} (s : type-Ω² a)
   where
 
-  3-loop-eckmann-hilton-Ω² :
-    type-Ω³ a
+  3-loop-eckmann-hilton-Ω² : type-Ω³ a
   3-loop-eckmann-hilton-Ω² =
     map-equiv-pointed-equiv
       ( pointed-equiv-2-loop-pointed-identity (Ω (A , a)) (s ∙ s))
       ( eckmann-hilton-Ω² s s)
 
-  3-loop-eckmann-hilton-inverse-Ω² :
-    type-Ω³ a
+  3-loop-eckmann-hilton-inverse-Ω² : type-Ω³ a
   3-loop-eckmann-hilton-inverse-Ω² =
     map-equiv-pointed-equiv
       ( pointed-equiv-2-loop-pointed-identity (Ω (A , a)) (s ∙ s))
@@ -371,16 +363,14 @@ module _
   Id-inv-3-loop-eckmann-hilton-inverse-Ω²-3-loop-eckmann-hilton-Ω² :
     inv (3-loop-eckmann-hilton-inverse-Ω² s) ＝ 3-loop-eckmann-hilton-Ω² s
   Id-inv-3-loop-eckmann-hilton-inverse-Ω²-3-loop-eckmann-hilton-Ω² =
-    concat
-      ( inv
-        ( preserves-inv-map-Ω
-          ( pointed-map-pointed-equiv
-            ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s)))
-          (eckmann-hilton-inverse-Ω² s s)))
-      ( _)
-      ( ap
-        ( map-Ω
-          ( pointed-map-pointed-equiv
-            ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s))))
-        ( eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² s s))
+    ( inv
+      ( preserves-inv-map-Ω
+        ( pointed-map-pointed-equiv
+          ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s)))
+        (eckmann-hilton-inverse-Ω² s s))) ∙
+    ( ap
+      ( map-Ω
+        ( pointed-map-pointed-equiv
+          ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s))))
+      ( eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² s s))
 ```
diff --git a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md
index 755771796b..71471914a3 100644
--- a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md
+++ b/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 (λ ω → left-unit-law-horizontal-concat-Id² ω) α) ∙
+    ( ( inv-nat-htpy (λ ω → compute-left-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 (λ ω → right-unit-law-horizontal-concat-Id² ω) α) ∙
+    ( ( inv-nat-htpy (λ ω → compute-right-horizontal-concat-Id² ω) α) ∙
       ( left-unit ∙
         ( ( inv right-unit) ∙
           ( ( inv-nat-htpy

From 202742e180a1c1353f6385173db9804fe0e44fe0 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Fri, 9 Feb 2024 15:43:25 +0100
Subject: [PATCH 04/14] try stuff and get nowhere

---
 src/foundation/path-algebra.lagda.md          |  24 ++-
 ...ing-identifications-concatenation.lagda.md |   7 +-
 src/foundation/yoneda-identity-types.lagda.md |  35 +++-
 .../double-loop-spaces.lagda.md               |  35 ++--
 .../eckmann-hilton-argument.lagda.md          | 159 +++++++-----------
 5 files changed, 127 insertions(+), 133 deletions(-)

diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
index 1f3a4b8a7e..d587b6529b 100644
--- a/src/foundation/path-algebra.lagda.md
+++ b/src/foundation/path-algebra.lagda.md
@@ -282,7 +282,21 @@ interchange-Id² :
   ( vertical-concat-Id²
     ( horizontal-concat-Id² α γ)
     ( horizontal-concat-Id² β δ))
-interchange-Id² refl refl refl refl = refl
+interchange-Id² refl _ refl _ = refl
+
+inner-interchange-Id² :
+  {l : Level} {A : UU l} {x y z : A} {p r : x ＝ y} {u v : y ＝ z}
+  (β : 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² β
+
+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² δ
 
 unit-law-α-interchange-Id² :
   {l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} (α : p ＝ q) (u : y ＝ z) →
@@ -290,12 +304,12 @@ unit-law-α-interchange-Id² :
     ( right-unit ∙ compute-right-horizontal-concat-Id² α)) ＝
   ( ( compute-right-horizontal-concat-Id² (α ∙ refl)) ∙
     ( ap (λ s → right-whisker-concat s u) right-unit))
-unit-law-α-interchange-Id² refl u = refl
+unit-law-α-interchange-Id² refl _ = refl
 
 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 ＝ refl
-unit-law-β-interchange-Id² refl u = refl
+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) →
@@ -303,12 +317,12 @@ unit-law-γ-interchange-Id² :
     ( right-unit ∙ compute-left-horizontal-concat-Id² γ)) ＝
   ( ( compute-left-horizontal-concat-Id² (γ ∙ refl)) ∙
     ( ap (left-whisker-concat p) right-unit))
-unit-law-γ-interchange-Id² p refl = refl
+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 δ ＝ refl
-unit-law-δ-interchange-Id² p refl = refl
+unit-law-δ-interchange-Id² _ refl = refl
 ```
 
 ## Properties of 3-paths
diff --git a/src/foundation/whiskering-identifications-concatenation.lagda.md b/src/foundation/whiskering-identifications-concatenation.lagda.md
index 661b2b9c4e..e60a0e1a3b 100644
--- a/src/foundation/whiskering-identifications-concatenation.lagda.md
+++ b/src/foundation/whiskering-identifications-concatenation.lagda.md
@@ -242,8 +242,7 @@ module _
     {q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') →
     inv (commutative-right-whisker-left-whisker-concat α β) ＝
     commutative-left-whisker-right-whisker-concat β α
-  compute-inv-commutative-left-whisker-right-whisker-concat refl refl =
-    refl
+  compute-inv-commutative-left-whisker-right-whisker-concat refl refl = refl
 ```
 
 ### Swapping the order of left and right whiskering of identifications
@@ -280,7 +279,7 @@ module _
     {a b c d : A} (p : a ＝ b) {r s : b ＝ c} (t : r ＝ s) (q : c ＝ d) →
     double-whisker-concat p t q ∙ assoc p s q ＝
     assoc p r q ∙ double-whisker-concat' p t q
-  swap-double-whisker-concat refl refl refl = refl
+  swap-double-whisker-concat refl refl _ = refl
 ```
 
 ### The action on identifications of concatenating by `refl` on the right
@@ -349,7 +348,7 @@ module _
   compute-inv-left-whisker-concat :
     {a b c : A} (p : a ＝ b) {q r : b ＝ c} (s : q ＝ r) →
     left-whisker-concat p (inv s) ＝ inv (left-whisker-concat p s)
-  compute-inv-left-whisker-concat p s = ap-inv (concat p _) s
+  compute-inv-left-whisker-concat p = ap-inv (concat p _)
 ```
 
 ### Right whiskering of identifications commutes with inverses of identifications
diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 9a139f3a84..770304a665 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -691,8 +691,8 @@ module _
   ap-yoneda-Id : {x y : A} → x ＝ʸ y → f x ＝ʸ f y
   ap-yoneda-Id = yoneda-eq-eq ∘ eq-ap-yoneda-Id
 
-  compute-ap-reflʸ : {x : A} → ap-yoneda-Id (reflʸ {x = x}) ＝ reflʸ
-  compute-ap-reflʸ = refl
+  compute-ap-refl-yoneda-Id : {x : A} → ap-yoneda-Id (reflʸ {x = x}) ＝ reflʸ
+  compute-ap-refl-yoneda-Id = refl
 
 module _
   {l1 : Level} {A : UU l1}
@@ -757,8 +757,8 @@ module _
   tr-yoneda-Id : {x y : A} → x ＝ʸ y → B x → B y
   tr-yoneda-Id = tr B ∘ eq-yoneda-eq
 
-  compute-tr-reflʸ : {x : A} → tr-yoneda-Id (reflʸ {x = x}) ＝ id
-  compute-tr-reflʸ = refl
+  compute-tr-refl-yoneda-Id : {x : A} → tr-yoneda-Id (reflʸ {x = x}) ＝ id
+  compute-tr-refl-yoneda-Id = refl
 ```
 
 ### Standard function extensionality with respect to Yoneda identifications
@@ -813,6 +813,33 @@ module _
   is-equiv-yoneda-eq-equiv = is-equiv-map-equiv equiv-yoneda-eq-equiv
 ```
 
+### Whiskering of Yoneda identifications
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z : A}
+  where
+
+  right-whisker-concat-yoenda-Id' :
+    {p q : x ＝ y} → p ＝ʸ q → (r : y ＝ z) → p ∙ᵣ r ＝ʸ q ∙ᵣ r
+  right-whisker-concat-yoenda-Id' α refl _ t = t ∙ eq-yoneda-eq α
+
+  right-whisker-concat-yoenda-Id :
+    {p q : x ＝ʸ y} → p ＝ʸ q → (r : y ＝ʸ z) → p ∙ʸ r ＝ʸ q ∙ʸ r
+  right-whisker-concat-yoenda-Id α r = ap-yoneda-Id (_∙ʸ r) α
+
+module _
+  {l : Level} {A : UU l}
+  where
+
+  right-unit-law-right-whisker-concat-yoenda-Id' :
+    {x y : A} {p q : x ＝ y} (α : p ＝ʸ q) →
+    right-whisker-concat-yoenda-Id' α refl ＝ α
+  right-unit-law-right-whisker-concat-yoenda-Id' α =
+    eq-multivariable-htpy 2
+      ( λ _ t → inv (commutative-preconcat-refl-Id-yoneda-Id α t))
+```
+
 ### Horizontal concatenation of Yoneda identifications
 
 ```agda
diff --git a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
index a32fc552af..52379055f0 100644
--- a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
+++ b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
@@ -42,7 +42,7 @@ module _
   Ω² A = iterated-loop-space 2 A
 
   type-Ω² : {A : UU l} (a : A) → UU l
-  type-Ω² a = Id (refl {x = a}) (refl {x = a})
+  type-Ω² a = refl {x = a} ＝ refl {x = a}
 
   refl-Ω² : {A : UU l} {a : A} → type-Ω² a
   refl-Ω² = refl
@@ -70,23 +70,21 @@ module _
   where
 
   left-unit-law-vertical-concat-Ω² :
-    {a : A} {α : type-Ω² a} →
-    Id (vertical-concat-Ω² refl-Ω² α) α
+    {a : A} {α : type-Ω² a} → vertical-concat-Ω² refl-Ω² α ＝ α
   left-unit-law-vertical-concat-Ω² = left-unit
 
   right-unit-law-vertical-concat-Ω² :
-    {a : A} {α : type-Ω² a} →
-    Id (vertical-concat-Ω² α refl-Ω²) α
+    {a : A} {α : type-Ω² a} → vertical-concat-Ω² α refl-Ω² ＝ α
   right-unit-law-vertical-concat-Ω² = right-unit
 
   left-unit-law-horizontal-concat-Ω² :
     {a : A} {α : type-Ω² a} →
-    Id (horizontal-concat-Ω² refl-Ω² α) α
+    horizontal-concat-Ω² refl-Ω² α ＝ α
   left-unit-law-horizontal-concat-Ω² {α = α} =
-    ( compute-left-horizontal-concat-Id² α) ∙ (ap-id α)
+    compute-left-horizontal-concat-Id² α ∙ ap-id α
 
   naturality-right-unit :
-    {x y : A} {p q : Id x y} (α : Id p q) →
+    {x y : A} {p q : x ＝ y} (α : p ＝ q) →
     coherence-square-identifications
       ( right-unit)
       ( right-whisker-concat α refl)
@@ -95,25 +93,21 @@ module _
   naturality-right-unit {p = refl} refl = refl
 
   naturality-right-unit-Ω² :
-    {x : A} (α : type-Ω² x) →
-    right-whisker-concat α refl ＝ α
+    {x : A} (α : type-Ω² x) → right-whisker-concat α refl ＝ α
   naturality-right-unit-Ω² α = inv right-unit ∙ naturality-right-unit α
 
   right-unit-law-horizontal-concat-Ω² :
-    {a : A} {α : type-Ω² a} →
-    Id (horizontal-concat-Ω² α refl-Ω²) α
+    {a : A} {α : type-Ω² a} → horizontal-concat-Ω² α refl-Ω² ＝ α
   right-unit-law-horizontal-concat-Ω² {α = α} =
-    ( compute-right-horizontal-concat-Id² α) ∙ (naturality-right-unit-Ω² α)
+    compute-right-horizontal-concat-Id² α ∙ naturality-right-unit-Ω² α
 
   left-unit-law-left-whisker-Ω² :
-    {a : A} (α : type-Ω² a) →
-    left-whisker-concat (refl-Ω (pair A a)) α ＝ α
+    {a : A} (α : type-Ω² a) → left-whisker-concat (refl-Ω (A , a)) α ＝ α
   left-unit-law-left-whisker-Ω² α =
     left-unit-law-left-whisker-concat α
 
   right-unit-law-right-whisker-Ω² :
-    {a : A} (α : type-Ω² a) →
-    right-whisker-concat α (refl-Ω (pair A a)) ＝ α
+    {a : A} (α : type-Ω² a) → right-whisker-concat α (refl-Ω (A , a)) ＝ α
   right-unit-law-right-whisker-Ω² α =
     inv (right-unit-law-right-whisker-concat α ∙ right-unit)
 ```
@@ -126,7 +120,7 @@ interchange-Ω² :
   Id
     ( horizontal-concat-Ω² (vertical-concat-Ω² α β) (vertical-concat-Ω² γ δ))
     ( vertical-concat-Ω² (horizontal-concat-Ω² α γ) (horizontal-concat-Ω² β δ))
-interchange-Ω² α β γ δ = interchange-Id² α β γ δ
+interchange-Ω² = interchange-Id²
 ```
 
 ## Properties
@@ -140,8 +134,7 @@ module _
   where
 
   pointed-equiv-2-loop-pointed-identity :
-    Ω (pair (point-Pointed-Type A ＝ x) p) ≃∗ Ω² A
+    Ω (point-Pointed-Type A ＝ x , p) ≃∗ Ω² A
   pointed-equiv-2-loop-pointed-identity =
-    pointed-equiv-Ω-pointed-equiv
-      ( pointed-equiv-loop-pointed-identity A p)
+    pointed-equiv-Ω-pointed-equiv (pointed-equiv-loop-pointed-identity A p)
 ```
diff --git a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
index fd4281dffe..222383bae5 100644
--- a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
+++ b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
@@ -1,4 +1,4 @@
-# The Eckmann-Hilton Argument
+# The Eckmann-Hilton argument
 
 ```agda
 module synthetic-homotopy-theory.eckmann-hilton-argument where
@@ -30,15 +30,15 @@ open import synthetic-homotopy-theory.triple-loop-spaces
 
 There are two classical statements of the Eckmann-Hilton argument. The first
 states that a group object in the category of groups is abelian. The second
-states that `π₂ (X)` is abelian, for any space `X`. The former is an algebraic
+states that `π₂(X)` is abelian, for any space `X`. The former is an algebraic
 statement, while the latter is a homotopy theoretic statment. As it turns out,
 the two are equivalent. See the following
 [wikipedia article](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument#Two-dimensional_proof).
 
-Both these phrasing, however, are about set level structures. Since we have
-access to untruncated types, it is more natural to prove untruncated analogs of
-the above two statements. Thus, we will work with the following statement of the
-Eckmann-Hilton argument:
+Both these phrasings, however, are about set level structures. Since we have
+access to untruncated types, it is more natural to consider untruncated analogs
+of the above two statements. Thus, we will work with the following statement of
+the Eckmann-Hilton argument:
 
 `(α β : Ω² X) → α ∙ β = β ∙ α`
 
@@ -171,22 +171,14 @@ module _
   eckmann-hilton-Ω² :
     (α β : type-Ω² (point-Pointed-Type A)) → α ∙ β ＝ β ∙ α
   eckmann-hilton-Ω² α β =
-    equational-reasoning
-    (α ∙ β) ＝
-    ( left-whisker-concat refl α ∙ right-whisker-concat β refl)
-    by
-      ( inv
-        ( horizontal-concat-Id²
-          ( left-unit-law-left-whisker-Ω² α)
-          ( right-unit-law-right-whisker-Ω² β)))
-    ＝ ( right-whisker-concat β refl) ∙
-      ( left-whisker-concat refl α)
-    by ( commutative-left-whisker-right-whisker-concat α β)
-    ＝ β ∙ α
-    by
+    ( inv
       ( horizontal-concat-Id²
-        ( right-unit-law-right-whisker-Ω² β)
-        ( left-unit-law-left-whisker-Ω² α))
+        ( left-unit-law-left-whisker-Ω² α)
+        ( right-unit-law-right-whisker-Ω² β))) ∙
+    ( commutative-left-whisker-right-whisker-concat α β) ∙
+    ( horizontal-concat-Id²
+      ( right-unit-law-right-whisker-Ω² β)
+      ( left-unit-law-left-whisker-Ω² α))
 ```
 
 #### Using right whiskering
@@ -199,7 +191,7 @@ braids `α` under `β`. This difference shows up nicely in the type theory. The
 first version uses the naturality of the operation of whiskering on the left,
 while the second version uses the naturality of the operation of whiskering on
 the right. Based on the intution of braiding, we should expect these two version
-of the Eckmann-Hilton identification to naturally "undo" each other, which the
+of the Eckmann-Hilton identification to naturally "undo" each other, which they
 do. Thus, we will refer to this alternate construction of Eckmann-Hilton as "the
 inverse Eckmann-Hilton argument", and the corresponding identification "the
 inverse Eckmann-Hilton identification".
@@ -209,24 +201,17 @@ module _
   {l : Level} {A : Pointed-Type l}
   where
 
-  eckmann-hilton-inverse-Ω² :
+  inv-eckmann-hilton-Ω² :
     (α β : type-Ω² (point-Pointed-Type A)) → α ∙ β ＝ β ∙ α
-  eckmann-hilton-inverse-Ω² α β =
-    equational-reasoning
-    (α ∙ β)
-    ＝ (right-whisker-concat α refl ∙ left-whisker-concat refl β)
-    by
-      ( inv
-        ( horizontal-concat-Id²
-          ( right-unit-law-right-whisker-Ω² α)
-          ( left-unit-law-left-whisker-Ω² β)))
-    ＝ (left-whisker-concat refl β ∙ right-whisker-concat α refl)
-    by commutative-right-whisker-left-whisker-concat α β
-    ＝ β ∙ α
-    by
+  inv-eckmann-hilton-Ω² α β =
+    ( inv
       ( horizontal-concat-Id²
-        ( left-unit-law-left-whisker-Ω² β)
-        ( right-unit-law-right-whisker-Ω² α))
+        ( right-unit-law-right-whisker-Ω² α)
+        ( left-unit-law-left-whisker-Ω² β))) ∙
+    ( commutative-right-whisker-left-whisker-concat α β) ∙
+    ( horizontal-concat-Id²
+      ( left-unit-law-left-whisker-Ω² β)
+      ( right-unit-law-right-whisker-Ω² α))
 ```
 
 We now prove that this Eckmann-Hilton identification "undoes" the previously
@@ -234,40 +219,28 @@ constructed Eckmann-Hilton identification. If we think of braiding `α` over `β
 then braiding `β` under `α`, we should end up with the trivial braid. Thus, we
 should have
 
-`eckmann-hilton-Ω² α β ∙ eckman-hilton-inverse-Ω² β α ＝ refl`
+`eckmann-hilton-Ω² α β ∙ inv-eckmann-hilton-Ω² β α ＝ refl`
 
 This is equivalent to,
 
-`inv eckman-hilton-inverse-Ω² β α ＝ eckmann-hilton-Ω² α β`
+`inv inv-eckmann-hilton-Ω² β α ＝ eckmann-hilton-Ω² α β`
+
+which is what we prove.
 
-which is what we prove. Note that the above property is distinct from syllepsis,
-since it concerns two different construction of the Eckmann-Hilton
-identification. Further, it works for all 2-loops, not just 3-loops.
+**Note.** that the above property is distinct from syllepsis, since it concerns
+two different construction of the Eckmann-Hilton identification. Further, it
+works for all 2-loops, not just 3-loops.
 
 ```agda
 module _
   {l : Level} {A : Pointed-Type l}
   where
 
-  eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² :
+  compute-inv-inv-eckmann-hilton-Ω² :
     (α β : type-Ω² (point-Pointed-Type A)) →
-    inv (eckmann-hilton-inverse-Ω² β α) ＝ (eckmann-hilton-Ω² α β)
-  eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² α β =
-    equational-reasoning
-    ( inv (eckmann-hilton-inverse-Ω² β α))
-    ＝
-        ( inv
-          ( horizontal-concat-Id²
-            ( left-unit-law-left-whisker-Ω² α)
-              ( right-unit-law-right-whisker-Ω² β))) ∙
-        ( inv
-          (
-            ( inv
-              ( horizontal-concat-Id²
-                ( right-unit-law-right-whisker-Ω² β)
-                ( left-unit-law-left-whisker-Ω² α))) ∙
-            ( commutative-right-whisker-left-whisker-concat β α)))
-    by distributive-inv-concat
+    inv (inv-eckmann-hilton-Ω² β α) ＝ eckmann-hilton-Ω² α β
+  compute-inv-inv-eckmann-hilton-Ω² α β =
+    ( distributive-inv-concat
       ( ( inv
           ( horizontal-concat-Id²
             ( right-unit-law-right-whisker-Ω² β)
@@ -275,19 +248,8 @@ module _
         ( commutative-right-whisker-left-whisker-concat β α))
       ( horizontal-concat-Id²
         ( left-unit-law-left-whisker-Ω² α)
-        ( right-unit-law-right-whisker-Ω² β))
-    ＝
-      ( inv
-        ( horizontal-concat-Id²
-          ( left-unit-law-left-whisker-Ω² α)
-            ( right-unit-law-right-whisker-Ω² β))) ∙
-      ( ( inv (commutative-right-whisker-left-whisker-concat β α)) ∙
-        ( inv
-          ( inv
-            ( horizontal-concat-Id²
-              ( right-unit-law-right-whisker-Ω² β)
-              ( left-unit-law-left-whisker-Ω² α)))))
-    by left-whisker-concat
+        ( right-unit-law-right-whisker-Ω² β))) ∙
+    ( left-whisker-concat
       ( inv
         ( horizontal-concat-Id²
           ( left-unit-law-left-whisker-Ω² α)
@@ -297,17 +259,8 @@ module _
           ( horizontal-concat-Id²
             ( right-unit-law-right-whisker-Ω² β)
             ( left-unit-law-left-whisker-Ω² α)))
-        ( commutative-right-whisker-left-whisker-concat β α))
-    ＝
-      ( inv
-        ( horizontal-concat-Id²
-          ( left-unit-law-left-whisker-Ω² α)
-            ( right-unit-law-right-whisker-Ω² β))) ∙
-      ( ( commutative-left-whisker-right-whisker-concat α β) ∙
-        ( horizontal-concat-Id²
-          ( right-unit-law-right-whisker-Ω² β)
-          ( left-unit-law-left-whisker-Ω² α)))
-    by left-whisker-concat
+        ( commutative-right-whisker-left-whisker-concat β α))) ∙
+    ( left-whisker-concat
       ( inv
         ( horizontal-concat-Id²
           ( left-unit-law-left-whisker-Ω² α)
@@ -317,10 +270,9 @@ module _
         ( inv-inv
           ( horizontal-concat-Id²
             ( right-unit-law-right-whisker-Ω² β)
-            ( left-unit-law-left-whisker-Ω² α))))
-    ＝ eckmann-hilton-Ω² α β
-    by inv (
-      assoc
+            ( left-unit-law-left-whisker-Ω² α))))) ∙
+    ( inv
+      ( assoc
         ( inv
           ( horizontal-concat-Id²
             ( left-unit-law-left-whisker-Ω² α)
@@ -328,12 +280,12 @@ module _
         ( commutative-left-whisker-right-whisker-concat α β)
         ( horizontal-concat-Id²
           ( right-unit-law-right-whisker-Ω² β)
-          ( left-unit-law-left-whisker-Ω² α)))
+          ( left-unit-law-left-whisker-Ω² α))))
 ```
 
 ## Properties
 
-### We can apply each `eckmann-hilton-Ω²` and `eckmann-hilton-inverse-Ω²` to a single 2-loop to obtain a 3-loop
+### We can apply each `eckmann-hilton-Ω²` and `inv-eckmann-hilton-Ω²` to a single 2-loop to obtain a 3-loop
 
 ```agda
 module _
@@ -346,11 +298,11 @@ module _
       ( pointed-equiv-2-loop-pointed-identity (Ω (A , a)) (s ∙ s))
       ( eckmann-hilton-Ω² s s)
 
-  3-loop-eckmann-hilton-inverse-Ω² : type-Ω³ a
-  3-loop-eckmann-hilton-inverse-Ω² =
+  inv-3-loop-eckmann-hilton-Ω² : type-Ω³ a
+  inv-3-loop-eckmann-hilton-Ω² =
     map-equiv-pointed-equiv
       ( pointed-equiv-2-loop-pointed-identity (Ω (A , a)) (s ∙ s))
-      ( eckmann-hilton-inverse-Ω² s s)
+      ( inv-eckmann-hilton-Ω² s s)
 ```
 
 ### The above two 3-loops are inverses
@@ -360,17 +312,26 @@ module _
   {l : Level} {A : UU l} {a : A} (s : type-Ω² a)
   where
 
-  Id-inv-3-loop-eckmann-hilton-inverse-Ω²-3-loop-eckmann-hilton-Ω² :
-    inv (3-loop-eckmann-hilton-inverse-Ω² s) ＝ 3-loop-eckmann-hilton-Ω² s
-  Id-inv-3-loop-eckmann-hilton-inverse-Ω²-3-loop-eckmann-hilton-Ω² =
+  compute-inv-inv-3-loop-eckmann-hilton-Ω² :
+    inv (inv-3-loop-eckmann-hilton-Ω² s) ＝ 3-loop-eckmann-hilton-Ω² s
+  compute-inv-inv-3-loop-eckmann-hilton-Ω² =
     ( inv
       ( preserves-inv-map-Ω
         ( pointed-map-pointed-equiv
           ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s)))
-        (eckmann-hilton-inverse-Ω² s s))) ∙
+        (inv-eckmann-hilton-Ω² s s))) ∙
     ( ap
       ( map-Ω
         ( pointed-map-pointed-equiv
           ( pointed-equiv-loop-pointed-identity (Ω (A , a)) (s ∙ s))))
-      ( eckmann-hilton-inverse-Ω²-undoes-eckmann-hilton-Ω² s s))
+      ( compute-inv-inv-eckmann-hilton-Ω² s s))
 ```
+
+## External links
+
+- [The Eckmann-Hilton argument](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument)
+  at 1Lab.
+- [Eckmann-Hilton argument](https://ncatlab.org/nlab/show/Eckmann-Hilton+argument)
+  at $n$Lab.
+- [Eckmann-Hilton argument](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument)
+  at Wikipedia.

From 99ca7c5e76f0d7599571b8bf78acca4746fcda2e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 14 Feb 2024 12:31:46 +0100
Subject: [PATCH 05/14] nitpick

---
 src/foundation/yoneda-identity-types.lagda.md | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 770304a665..badc7ea6f9 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -890,7 +890,7 @@ and
 ```
 
 live in the same type. Hence, we can pose the question of whether the horizontal
-concatenation operation is associative, which it is weakly:
+concatenation operation is associative, which it is, albeit weakly:
 
 ```agda
 module _
@@ -906,12 +906,8 @@ module _
   assoc-horizontal-concat-yoneda-Id² {p} α {q} β γ =
     ind-yoneda-Id
       ( λ _ α →
-        ( horizontal-concat-yoneda-Id²
-          ( horizontal-concat-yoneda-Id² α β)
-          ( γ)) ＝
-        ( horizontal-concat-yoneda-Id²
-          ( α)
-          ( horizontal-concat-yoneda-Id² β γ)))
+        ( horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² α β) γ) ＝
+        ( horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ)))
       ( ind-yoneda-Id
         ( λ _ β →
           ( horizontal-concat-yoneda-Id²

From ab394b9e080138492451507e927cbbf78063049f Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 14 Feb 2024 12:33:34 +0100
Subject: [PATCH 06/14] self-review

---
 src/foundation/yoneda-identity-types.lagda.md                 | 4 ----
 .../eckmann-hilton-argument.lagda.md                          | 4 ++--
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index badc7ea6f9..779884b147 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -820,10 +820,6 @@ module _
   {l : Level} {A : UU l} {x y z : A}
   where
 
-  right-whisker-concat-yoenda-Id' :
-    {p q : x ＝ y} → p ＝ʸ q → (r : y ＝ z) → p ∙ᵣ r ＝ʸ q ∙ᵣ r
-  right-whisker-concat-yoenda-Id' α refl _ t = t ∙ eq-yoneda-eq α
-
   right-whisker-concat-yoenda-Id :
     {p q : x ＝ʸ y} → p ＝ʸ q → (r : y ＝ʸ z) → p ∙ʸ r ＝ʸ q ∙ʸ r
   right-whisker-concat-yoenda-Id α r = ap-yoneda-Id (_∙ʸ r) α
diff --git a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
index 222383bae5..7291099e07 100644
--- a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
+++ b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
@@ -329,8 +329,8 @@ module _
 
 ## External links
 
-- [The Eckmann-Hilton argument](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument)
-  at 1Lab.
+- [The Eckmann-Hilton argument](https://1lab.dev/Algebra.Magma.Unital.EckmannHilton.html)
+  at 1lab.
 - [Eckmann-Hilton argument](https://ncatlab.org/nlab/show/Eckmann-Hilton+argument)
   at $n$Lab.
 - [Eckmann-Hilton argument](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument)

From 9e2b779f1937cd33402ae13be23cdcfb6b7ade0d Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 14 Feb 2024 12:45:26 +0100
Subject: [PATCH 07/14] left whiskering yoneda ids

---
 src/foundation/yoneda-identity-types.lagda.md | 52 ++++++++-----------
 1 file changed, 22 insertions(+), 30 deletions(-)

diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 779884b147..94a62c4467 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -712,19 +712,19 @@ Using one of the two sides in the Gray interchange diagram
 
 ```text
                          ap (f x) q
-                 f x y -------------- f x y'
+                 f x y -------------> f x y'
                    |                    |
                    |                    |
   ap (r ↦ f r y) p |                    | ap (r ↦ f r y') p
                    |                    |
-                   |                    |
-                 f x' y ------------- f x' y'
+                   ∨                    ∨
+                 f x' y ------------> f x' y'
                          ap (f x') q
 ```
 
 and the fact that the concatenation operation on Yoneda identifications is
 two-sided strictly unital, we obtain an action of binary functions on Yoneda
-identifications that computes on both inputs.
+identifications that computes on both arguments.
 
 ```agda
 module _
@@ -820,20 +820,13 @@ module _
   {l : Level} {A : UU l} {x y z : A}
   where
 
+  left-whisker-concat-yoenda-Id :
+    (p : x ＝ʸ y) {q r : y ＝ʸ z} → q ＝ʸ r → p ∙ʸ q ＝ʸ p ∙ʸ r
+  left-whisker-concat-yoenda-Id p β = ap-yoneda-Id (p ∙ʸ_) β
+
   right-whisker-concat-yoenda-Id :
     {p q : x ＝ʸ y} → p ＝ʸ q → (r : y ＝ʸ z) → p ∙ʸ r ＝ʸ q ∙ʸ r
   right-whisker-concat-yoenda-Id α r = ap-yoneda-Id (_∙ʸ r) α
-
-module _
-  {l : Level} {A : UU l}
-  where
-
-  right-unit-law-right-whisker-concat-yoenda-Id' :
-    {x y : A} {p q : x ＝ y} (α : p ＝ʸ q) →
-    right-whisker-concat-yoenda-Id' α refl ＝ α
-  right-unit-law-right-whisker-concat-yoenda-Id' α =
-    eq-multivariable-htpy 2
-      ( λ _ t → inv (commutative-preconcat-refl-Id-yoneda-Id α t))
 ```
 
 ### Horizontal concatenation of Yoneda identifications
@@ -885,8 +878,8 @@ and
   horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ)
 ```
 
-live in the same type. Hence, we can pose the question of whether the horizontal
-concatenation operation is associative, which it is, albeit weakly:
+inhabit the same type. Therefore, we can pose the question of whether the
+horizontal concatenation operation is associative, which it is, albeit weakly:
 
 ```agda
 module _
@@ -899,31 +892,30 @@ module _
     {r r' : z ＝ʸ w} (γ : r ＝ʸ r') →
     horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² α β) γ ＝
     horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ)
-  assoc-horizontal-concat-yoneda-Id² {p} α {q} β γ =
+  assoc-horizontal-concat-yoneda-Id² α {q} β {r} =
     ind-yoneda-Id
-      ( λ _ α →
+      ( λ _ γ →
         ( horizontal-concat-yoneda-Id² (horizontal-concat-yoneda-Id² α β) γ) ＝
         ( horizontal-concat-yoneda-Id² α (horizontal-concat-yoneda-Id² β γ)))
       ( ind-yoneda-Id
         ( λ _ β →
           ( horizontal-concat-yoneda-Id²
-            ( horizontal-concat-yoneda-Id² reflʸ β)
-            ( γ)) ＝
+            ( horizontal-concat-yoneda-Id² α β)
+            ( reflʸ {x = r})) ＝
           ( horizontal-concat-yoneda-Id²
-            ( reflʸ)
-            ( horizontal-concat-yoneda-Id² β γ)))
+            ( α)
+            ( horizontal-concat-yoneda-Id² β (reflʸ {x = r}))))
         ( ind-yoneda-Id
-          ( λ _ γ →
+          ( λ _ α →
             ( horizontal-concat-yoneda-Id²
-              ( horizontal-concat-yoneda-Id² (reflʸ {x = p}) (reflʸ {x = q}))
-              ( γ)) ＝
+              ( horizontal-concat-yoneda-Id² α (reflʸ {x = q}))
+              ( reflʸ {x = r})) ＝
             ( horizontal-concat-yoneda-Id²
-              ( reflʸ {x = p})
-              ( horizontal-concat-yoneda-Id² (reflʸ {x = q}) γ)))
+              ( α)
+              ( horizontal-concat-yoneda-Id² (reflʸ {x = q}) (reflʸ {x = r}))))
           ( refl)
-          ( γ))
+          ( α))
         ( β))
-      ( α)
 ```
 
 ### Vertical concatenation of Yoneda identifications

From 8dc4cad0e83e4892f6ee14df3274d94ab1bd52c1 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 14 Feb 2024 12:50:12 +0100
Subject: [PATCH 08/14] remove unfinished code

---
 src/foundation/yoneda-identity-types.lagda.md | 19 -------------------
 1 file changed, 19 deletions(-)

diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 94a62c4467..436f7c6330 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -930,25 +930,6 @@ module _
   vertical-concat-yoneda-Id² α β = α ∙ʸ β
 ```
 
-### The interchange law for Yoneda identificatinos
-
-```agda
-module _
-  {l : Level} {A : UU l} {x y z : A}
-  where
-
-  -- interchange-yoneda-Id² :
-  --   {p q r : x ＝ʸ y} {u v w : y ＝ʸ z}
-  --   (α : p ＝ʸ q) (β : q ＝ʸ r) (γ : u ＝ʸ v) (δ : v ＝ʸ w) →
-  --   ( horizontal-concat-yoneda-Id²
-  --     ( vertical-concat-yoneda-Id² α β)
-  --     ( vertical-concat-yoneda-Id² γ δ)) ＝
-  --   ( vertical-concat-yoneda-Id²
-  --     ( horizontal-concat-yoneda-Id² α γ)
-  --     ( horizontal-concat-yoneda-Id² β δ))
-  -- interchange-yoneda-Id² α β γ δ = {!   !}
-```
-
 ## See also
 
 - [The strictly involutive identity types](foundation.strictly-involutive-identity-types.md)

From 9177a3f9627b85b6a82b97c6dce19b369d05132a Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Wed, 14 Feb 2024 12:53:24 +0100
Subject: [PATCH 09/14] a comment

---
 src/foundation/yoneda-identity-types.lagda.md | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 436f7c6330..766919b740 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -831,6 +831,10 @@ module _
 
 ### Horizontal concatenation of Yoneda identifications
 
+We define horizontal concatenation in such a way that it computes as left
+whiskering when the left-hand argument is `refl`, and computes as right
+whiskering when the right-hand argument is `refl`.
+
 ```agda
 module _
   {l : Level} {A : UU l} {x y z : A}
@@ -838,16 +842,18 @@ module _
 
   horizontal-concat-yoneda-Id² :
     {p q : x ＝ʸ y} → p ＝ʸ q → {u v : y ＝ʸ z} → u ＝ʸ v → p ∙ʸ u ＝ʸ q ∙ʸ v
-  horizontal-concat-yoneda-Id² α β = ap-binary-yoneda-Id (_∙ʸ_) α β
+  horizontal-concat-yoneda-Id² = ap-binary-yoneda-Id (_∙ʸ_)
 
   compute-left-horizontal-concat-yoneda-Id² :
     {p : x ＝ʸ y} {u v : y ＝ʸ z} (β : u ＝ʸ v) →
-    horizontal-concat-yoneda-Id² reflʸ β ＝ ap-yoneda-Id (p ∙ʸ_) β
+    horizontal-concat-yoneda-Id² reflʸ β ＝
+    left-whisker-concat-yoenda-Id p β
   compute-left-horizontal-concat-yoneda-Id² β = refl
 
   compute-right-horizontal-concat-yoneda-Id² :
     {p q : x ＝ʸ y} (α : p ＝ʸ q) {u : y ＝ʸ z} →
-    horizontal-concat-yoneda-Id² α (reflʸ {x = u}) ＝ ap-yoneda-Id (_∙ʸ u) α
+    horizontal-concat-yoneda-Id² α (reflʸ {x = u}) ＝
+    right-whisker-concat-yoenda-Id α u
   compute-right-horizontal-concat-yoneda-Id² α = refl
 
 module _

From 7e39a5b46aa3975baa07a7c1c331e166af91f1cf Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sat, 17 Feb 2024 11:46:18 +0100
Subject: [PATCH 10/14] Update src/foundation/yoneda-identity-types.lagda.md

---
 src/foundation/yoneda-identity-types.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 766919b740..4dd177bf74 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -578,7 +578,7 @@ module _
 
 ### The groupoidal laws for the Yoneda identity types
 
-As we may now observe, associativity and the unit laws holds by `refl`.
+As we may now observe, associativity and the unit laws hold by `refl`.
 
 ```agda
 module _

From 6db3a77164fa85e716eaf15d7b7b9257940839c1 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sat, 17 Feb 2024 11:48:47 +0100
Subject: [PATCH 11/14] Update src/foundation/yoneda-identity-types.lagda.md

---
 src/foundation/yoneda-identity-types.lagda.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 4dd177bf74..b7aec446dd 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -708,7 +708,8 @@ module _
 
 ### Action of binary functions on Yoneda identifications
 
-Using one of the two sides in the Gray interchange diagram
+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
 
 ```text
                          ap (f x) q
@@ -723,8 +724,7 @@ Using one of the two sides in the Gray interchange diagram
 ```
 
 and the fact that the concatenation operation on Yoneda identifications is
-two-sided strictly unital, we obtain an action of binary functions on Yoneda
-identifications that computes on both arguments.
+two-sided strictly unital.
 
 ```agda
 module _

From d746433edc2f9dc5f35bbb31b7ca3d227cb86d5e Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sat, 17 Feb 2024 11:58:08 +0100
Subject: [PATCH 12/14] add links eckmann-hilton

---
 .../eckmann-hilton-argument.lagda.md          | 28 +++++++++++--------
 1 file changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
index 7291099e07..c886b19c8c 100644
--- a/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
+++ b/src/synthetic-homotopy-theory/eckmann-hilton-argument.lagda.md
@@ -29,18 +29,22 @@ open import synthetic-homotopy-theory.triple-loop-spaces
 ## Idea
 
 There are two classical statements of the Eckmann-Hilton argument. The first
-states that a group object in the category of groups is abelian. The second
-states that `π₂(X)` is abelian, for any space `X`. The former is an algebraic
-statement, while the latter is a homotopy theoretic statment. As it turns out,
-the two are equivalent. See the following
-[wikipedia article](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument#Two-dimensional_proof).
-
-Both these phrasings, however, are about set level structures. Since we have
-access to untruncated types, it is more natural to consider untruncated analogs
-of the above two statements. Thus, we will work with the following statement of
-the Eckmann-Hilton argument:
-
-`(α β : Ω² X) → α ∙ β = β ∙ α`
+states that a group object in the
+[category of groups](group-theory.category-of-groups.md) is
+[abelian](group-theory.abelian-groups.md). The second states that `π₂(X)` is
+abelian, for any space `X`. The former is an algebraic statement, while the
+latter is a homotopy theoretic statment. As it turns out, the two are
+[equivalent](foundation.logical-equivalences.md). See the following
+[Wikipedia article](https://en.wikipedia.org/wiki/Eckmann%E2%80%93Hilton_argument#Two-dimensional_proof).
+
+Both of these phrasings, however, are about [set](foundation-core.sets.md) level
+structures. Since we have access to untruncated types, it is more natural to
+consider untruncated analogs of the above two statements. Thus, we will work
+with the following statement of the Eckmann-Hilton argument:
+
+```text
+  (α β : Ω² X) → α ∙ β = β ∙ α
+```
 
 For fixed 2-loops, we will call the resulting identification "the Eckmann-Hilton
 identification". In this file we will give two different constructions of this

From 6b009153baf1517f63ffe4d60277b9c14e2e9c00 Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Sat, 17 Feb 2024 12:11:14 +0100
Subject: [PATCH 13/14] add Gray interchange diagram in file about `ap-binary`

---
 ...-identifications-binary-functions.lagda.md | 31 ++++++++++++++-----
 src/foundation/yoneda-identity-types.lagda.md |  6 ++--
 2 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/src/foundation/action-on-identifications-binary-functions.lagda.md b/src/foundation/action-on-identifications-binary-functions.lagda.md
index 4930ebf1d7..f0dd34c389 100644
--- a/src/foundation/action-on-identifications-binary-functions.lagda.md
+++ b/src/foundation/action-on-identifications-binary-functions.lagda.md
@@ -28,6 +28,23 @@ Given a binary operation `f : A → B → C` and
 we call this the
 {{#concept "binary action on identifications of binary functions" Agda=ap-binary}}.
 
+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
+
+```text
+                      ap (r ↦ f x r) q
+                 f x y -------------> f x y'
+                   |                    |
+                   |                    |
+  ap (r ↦ f r y) p |                    | ap (r ↦ f r y') p
+                   |                    |
+                   ∨                    ∨
+                 f x' y ------------> f x' y'.
+                      ap (r ↦ f x' r) q
+```
+
 ## Definition
 
 ### The binary action on identifications of binary functions
@@ -39,7 +56,7 @@ module _
 
   ap-binary :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') → f x y ＝ f x' y'
-  ap-binary {x} {x'} p {y} {y'} q = ap (λ z → f z y) p ∙ ap (f x') q
+  ap-binary {x} {x'} p {y} {y'} q = ap (λ r → f r y) p ∙ ap (f x') q
 ```
 
 ## Properties
@@ -51,13 +68,13 @@ of the
 [unary action on identifications of functions](foundation.action-on-identifications-functions.md):
 
 ```text
-  ap-binary f p q ＝ ap (f (-) y) p ∙ ap (f x' (-)) q
+  ap-binary f p q ＝ ap (r ↦ f r y) p ∙ ap (r ↦ f x' r) q
 ```
 
 and
 
 ```text
-  ap-binary f p q ＝ ap (f x (-)) q ∙ ap (f (-) y') p.
+  ap-binary f p q ＝ ap (r ↦ f x r) q ∙ ap (r ↦ f r y') p.
 ```
 
 ```agda
@@ -67,12 +84,12 @@ module _
 
   triangle-ap-binary :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
-    ap-binary f p q ＝ ap (λ z → f z y) p ∙ ap (f x') q
+    ap-binary f p q ＝ ap (λ r → f r y) p ∙ ap (f x') q
   triangle-ap-binary _ _ = refl
 
   triangle-ap-binary' :
     {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
-    ap-binary f p q ＝ ap (f x) q ∙ ap (λ z → f z y') p
+    ap-binary f p q ＝ ap (f x) q ∙ ap (λ r → f r y') p
   triangle-ap-binary' refl refl = refl
 ```
 
@@ -92,7 +109,7 @@ module _
   left-unit-ap-binary _ = refl
 
   right-unit-ap-binary :
-    {x x' : A} (p : x ＝ x') {y : B} → ap-binary f p refl ＝ ap (λ z → f z y) p
+    {x x' : A} (p : x ＝ x') {y : B} → ap-binary f p refl ＝ ap (λ r → f r y) p
   right-unit-ap-binary refl = refl
 ```
 
@@ -120,7 +137,7 @@ module _
   where
 
   ap-binary-diagonal :
-    {x x' : A} (p : x ＝ x') → ap-binary f p p ＝ ap (λ a → f a a) p
+    {x x' : A} (p : x ＝ x') → ap-binary f p p ＝ ap (λ r → f r r) p
   ap-binary-diagonal refl = refl
 ```
 
diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index b7aec446dd..4ef08b761b 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/src/foundation/yoneda-identity-types.lagda.md
@@ -712,15 +712,15 @@ 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
 
 ```text
-                         ap (f x) q
+                      ap (r ↦ f x r) q
                  f x y -------------> f x y'
                    |                    |
                    |                    |
   ap (r ↦ f r y) p |                    | ap (r ↦ f r y') p
                    |                    |
                    ∨                    ∨
-                 f x' y ------------> f x' y'
-                         ap (f x') q
+                 f x' y ------------> f x' y'.
+                      ap (r ↦ f x' r) q
 ```
 
 and the fact that the concatenation operation on Yoneda identifications is

From 76f19688aec37421d90d7269ba201f5017f0fd3d Mon Sep 17 00:00:00 2001
From: Fredrik Bakke <fredrbak@gmail.com>
Date: Mon, 19 Feb 2024 12:23:32 +0100
Subject: [PATCH 14/14] review

---
 ...-identifications-binary-functions.lagda.md |  2 +-
 src/foundation/path-algebra.lagda.md          | 32 +++++++++++--------
 src/foundation/yoneda-identity-types.lagda.md |  2 +-
 .../double-loop-spaces.lagda.md               |  4 +--
 .../triple-loop-spaces.lagda.md               |  4 +--
 5 files changed, 24 insertions(+), 20 deletions(-)

diff --git a/src/foundation/action-on-identifications-binary-functions.lagda.md b/src/foundation/action-on-identifications-binary-functions.lagda.md
index f0dd34c389..d9d2b1d339 100644
--- a/src/foundation/action-on-identifications-binary-functions.lagda.md
+++ b/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
diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
index 00db01351b..f22f14f192 100644
--- a/src/foundation/path-algebra.lagda.md
+++ b/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}
diff --git a/src/foundation/yoneda-identity-types.lagda.md b/src/foundation/yoneda-identity-types.lagda.md
index 4ef08b761b..081408e0ba 100644
--- a/src/foundation/yoneda-identity-types.lagda.md
+++ b/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
diff --git a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
index 52379055f0..03c7e352fa 100644
--- a/src/synthetic-homotopy-theory/double-loop-spaces.lagda.md
+++ b/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)) α ＝ α
diff --git a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md b/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md
index 71471914a3..cdb70b73bf 100644
--- a/src/synthetic-homotopy-theory/triple-loop-spaces.lagda.md
+++ b/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