The left and right whiskering operations commute

MIXFIX-OPERATORS.md

@@ -153,7 +153,7 @@ Below, we outline a list of general rules when assigning associativities.
   associated regardless. For instance, one should never write
 
   ```agda
-  assoc : p ∙ (q ∙ r) ＝ p ∙ q ∙ r
+  assoc : p ∙ q ∙ r ＝ p ∙ (q ∙ r)
   ```
 
 - **Unique well-typed associativity**. When an operator only has one well-typed

src/foundation-core/whiskering-homotopies.lagda.md

@@ -258,7 +258,15 @@ module _
   ap-right-whisk-htpy α h = α ·r h
 ```
 
-### Left and right whiskering commute definitionally
+### The left and right whiskering operations commute
+
+We have the coherence
+
+```text
+  (h ·l H) ·r h' ~ f ·l (H ·r g)
+```
+
+and, in fact, this equation holds definitionally.
 
 ```agda
 module _
@@ -272,6 +280,6 @@ module _
     (h : {x : A} {y : B x} → C y → D y)
     (H : {x : A} → f {x} ~ g {x})
     (h' : (x : A) → B x) →
-    h ·l (H ·r h') ~ (h ·l H) ·r h'
+    (h ·l H) ·r h' ~ h ·l (H ·r h')
   coherence-left-right-whisk-htpy h H h' = refl-htpy
 ```