Rename symmetric reasoning combinators. Minimal set of changes (#2160)

CHANGELOG.md

@@ -849,6 +849,7 @@ Non-backwards compatible changes
  IO.Effectful
  IO.Instances
  ```
+
 ### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder`
 
 * Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its
@@ -989,6 +990,53 @@ Non-backwards compatible changes
  Relation.Binary.Reasoning.PartialOrder
  ```
 
+### More modular design of equational reasoning.
+
+* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports
+ a range of modules containing pre-existing reasoning combinator syntax.
+
+* This makes it possible to add new or rename existing reasoning combinators to a
+ pre-existing `Reasoning` module in just a couple of lines
+ (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`)
+
+* One pre-requisite for that is that `≡-Reasoning` has been moved from
+ `Relation.Binary.PropositionalEquality.Core` (which shouldn't be
+ imported anyway as it's a `Core` module) to 
+ `Relation.Binary.PropositionalEquality.Properties`.
+ It is still exported by `Relation.Binary.PropositionalEquality`.
+
+### Renaming of symmetric combinators for equational reasoning
+
+* We've had various complaints about the symmetric version of reasoning combinators 
+ that use the syntax `_R˘⟨_⟩_` for some relation `R`, (e.g. `_≡˘⟨_⟩_` and `_≃˘⟨_⟩_`)
+ introduced in `v1.0`. In particular:
+ 1. The symbol `˘` is hard to type.
+ 2. The symbol `˘` doesn't convey the direction of the equality
+ 3. The left brackets aren't vertically aligned with the left brackets of the non-symmetric version.
+
+* To address these problems we have renamed all the symmetric versions of the 
+ combinators from `_R˘⟨_⟩_` to `_R⟨_⟨_` (the direction of the last bracket is flipped
+ to indicate the quality goes from right to left).
+
+* The old combinators still exist but have been deprecated. However due to 
+ [Agda issue #5617](https:/agda/agda/issues/5617), the deprecation warnings
+ don't fire correctly. We will not remove the old combinators before the above issue is
+ addressed. However, we still encourage migrating to the new combinators!
+
+* On a Linux-based system, the following command was used to globally migrate all uses of the
+ old combinators to the new ones in the standard library itself. 
+ It *may* be useful when trying to migrate your own code:
+ ```bash
+ find . -type f -name "*.agda" -print0 | xargs -0 sed -i -e 's/˘⟨\(.*\)⟩/⟨\1⟨/g'
+ ```
+ USUAL CAVEATS: It has not been widely tested and the standard library developers are not 
+ responsible for the results of this command. It is strongly recommended you back up your 
+ work before you attempt to run it.
+
+* NOTE: this refactoring may require some extra bracketing around the operator `_⟨_⟩_` from 
+ `Function.Base` if the `_⟨_⟩_` operator is used within the reasoning proof. The symptom
+ for this is a `Don't know how to parse` error.
+
 ### Other
 
 * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
@@ -1228,21 +1276,6 @@ Major improvements
  * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module.
 
 * In `Relation.Binary.Reasoning.Base.Triple`, added a new parameter `<-irrefl : Irreflexive _≈_ _<_`
-
-### More modular design of equational reasoning.
-
-* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports
- a range of modules containing pre-existing reasoning combinator syntax.
-
-* This makes it possible to add new or rename existing reasoning combinators to a
- pre-existing `Reasoning` module in just a couple of lines
- (e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`)
-
-* One pre-requisite for that is that `≡-Reasoning` has been moved from
- `Relation.Binary.PropositionalEquality.Core` (which shouldn't be
- imported anyway as it's a `Core` module) to 
- `Relation.Binary.PropositionalEquality.Properties`.
- It is still exported by `Relation.Binary.PropositionalEquality`.
  
 Deprecated modules
 ------------------

README/Data/Fin/Relation/Unary/Top.agda

@@ -76,8 +76,8 @@ opposite-prop {suc n} i with view i
 ... | ‵fromℕ rewrite toℕ-fromℕ n | n∸n≡0 n = refl
 ... | ‵inject₁ j = begin
  suc (toℕ (opposite j)) ≡⟨ cong suc (opposite-prop j) ⟩
- suc (n ∸ suc (toℕ j)) ≡˘⟨ +-∸-assoc 1 (toℕ<n j) ⟩
- n ∸ toℕ j ≡˘⟨ cong (n ∸_) (toℕ-inject₁ j) ⟩
+ suc (n ∸ suc (toℕ j)) ≡⟨ +-∸-assoc 1 (toℕ<n j) ⟨
+ n ∸ toℕ j ≡⟨ cong (n ∸_) (toℕ-inject₁ j) ⟨
  n ∸ toℕ (inject₁ j) ∎ where open ≡-Reasoning
 
 ------------------------------------------------------------------------

README/Data/Vec/Relation/Binary/Equality/Cast.agda

@@ -86,7 +86,7 @@ example1a-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc
  cast eq (fromList (xs L.∷ʳ x)) ≡ fromList xs ∷ʳ x
 example1a-fromList-∷ʳ x xs eq = begin
  cast eq (fromList (xs L.∷ʳ x)) ≡⟨⟩
- cast eq (fromList (xs L.++ L.[ x ])) ≡˘⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟩
+ cast eq (fromList (xs L.++ L.[ x ])) ≡⟨ cast-trans eq₁ eq₂ (fromList (xs L.++ L.[ x ])) ⟨
  cast eq₂ (cast eq₁ (fromList (xs L.++ L.[ x ]))) ≡⟨ cong (cast eq₂) (fromList-++ xs) ⟩
  cast eq₂ (fromList xs ++ [ x ]) ≡⟨ ≈-sym (unfold-∷ʳ (sym eq₂) x (fromList xs)) ⟩
  fromList xs ∷ʳ x ∎
@@ -105,7 +105,7 @@ example1b-fromList-∷ʳ : ∀ (x : A) xs .(eq : L.length (xs L.∷ʳ x) ≡ suc
 example1b-fromList-∷ʳ x xs eq = begin
  fromList (xs L.∷ʳ x) ≈⟨⟩
  fromList (xs L.++ L.[ x ]) ≈⟨ fromList-++ xs ⟩
- fromList xs ++ [ x ] ≈˘⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟩
+ fromList xs ++ [ x ] ≈⟨ unfold-∷ʳ (+-comm 1 (L.length xs)) x (fromList xs) ⟨
  fromList xs ∷ʳ x ∎
  where open CastReasoning
 
@@ -120,10 +120,10 @@ example1b-fromList-∷ʳ x xs eq = begin
 -- ≈-trans : xs ≈[ m≡n ] ys → ys ≈[ n≡o ] zs → xs ≈[ trans m≡n n≡o ] zs
 -- Accordingly, `_≈[_]_` admits the standard set of equational reasoning
 -- combinators. Suppose `≈-eqn : xs ≈[ m≡n ] ys`,
--- xs ≈⟨ ≈-eqn  ⟩ -- `_≈⟨_⟩_` takes a `_≈[_]_` step, adjusting
--- ys  -- the index at the same time
+-- xs ≈⟨ ≈-eqn ⟩ -- `_≈⟨_⟩_` takes a `_≈[_]_` step, adjusting
+-- ys -- the index at the same time
 --
--- ys ≈˘⟨ ≈-eqn ⟩ -- `_≈˘⟨_⟩_` takes a symmetric `_≈[_]_` step
+-- ys ≈⟨ ≈-eqn ⟨ -- `_≈⟨_⟨_` takes a symmetric `_≈[_]_` step
 -- xs
 example2a : ∀ .(eq : suc m + n ≡ m + suc n) (xs : Vec A m) a ys →
  cast eq ((reverse xs ∷ʳ a) ++ ys) ≡ reverse xs ++ (a ∷ ys)
@@ -138,7 +138,7 @@ example2a eq xs a ys = begin
 -- xs ≂⟨ ≡-eqn ⟩ -- Takes a `_≡_` step; no change to the index
 -- ys
 --
--- ys ≂˘⟨ ≡-eqn ⟩ -- Takes a symmetric `_≡_` step
+-- ys ≂⟨ ≡-eqn ⟨ -- Takes a symmetric `_≡_` step
 -- xs
 -- Equivalently, `≈-reflexive` injects `_≡_` into `_≈[_]_`. That is,
 -- `xs ≂⟨ ≡-eqn ⟩ ys` is the same as `xs ≈⟨ ≈-reflexive ≡-eqn ⟩ ys`.
@@ -149,7 +149,7 @@ example2b eq xs a ys = begin
  (a ∷ xs) ʳ++ ys ≂⟨ unfold-ʳ++ (a ∷ xs) ys ⟩ -- index: suc m + n
  reverse (a ∷ xs) ++ ys ≂⟨ cong (_++ ys) (reverse-∷ a xs) ⟩ -- index: suc m + n
  (reverse xs ∷ʳ a) ++ ys ≈⟨ ∷ʳ-++ eq a (reverse xs) ⟩ -- index: suc m + n
- reverse xs ++ (a ∷ ys) ≂˘⟨ unfold-ʳ++ xs (a ∷ ys) ⟩ -- index: m + suc n
+ reverse xs ++ (a ∷ ys) ≂⟨ unfold-ʳ++ xs (a ∷ ys) ⟨ -- index: m + suc n
  xs ʳ++ (a ∷ ys) ∎ -- index: m + suc n
  where open CastReasoning
 
@@ -201,11 +201,11 @@ example3b-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
 example4-cong² : ∀ .(eq : (m + 1) + n ≡ n + suc m) a (xs : Vec A m) ys →
  cast eq (reverse ((xs ++ [ a ]) ++ ys)) ≡ ys ʳ++ reverse (xs ∷ʳ a)
 example4-cong² {m = m} {n} eq a xs ys = begin
- reverse ((xs ++ [ a ]) ++ ys) ≈˘⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
+ reverse ((xs ++ [ a ]) ++ ys) ≈⟨ ≈-cong reverse (cast-reverse (cong (_+ n) (+-comm 1 m)) ((xs ∷ʳ a) ++ ys))
  (≈-cong (_++ ys) (cast-++ˡ (+-comm 1 m) (xs ∷ʳ a))
- (unfold-∷ʳ _ a xs)) ⟩
+ (unfold-∷ʳ _ a xs)) ⟨
  reverse ((xs ∷ʳ a) ++ ys) ≈⟨ reverse-++ (+-comm (suc m) n) (xs ∷ʳ a) ys ⟩
- reverse ys ++ reverse (xs ∷ʳ a) ≂˘⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟩
+ reverse ys ++ reverse (xs ∷ʳ a) ≂⟨ unfold-ʳ++ ys (reverse (xs ∷ʳ a)) ⟨
  ys ʳ++ reverse (xs ∷ʳ a) ∎
  where open CastReasoning
 
@@ -237,7 +237,7 @@ example5-fromList-++-++′ {xs = xs} {ys} {zs} eq = begin
 -- and then switch to the reasoning system of `_≈[_]_`.
 example6a-reverse-∷ʳ : ∀ x (xs : Vec A n) → reverse (xs ∷ʳ x) ≡ x ∷ reverse xs
 example6a-reverse-∷ʳ {n = n} x xs = begin-≡
- reverse (xs ∷ʳ x) ≡˘⟨ ≈-reflexive refl ⟩
+ reverse (xs ∷ʳ x) ≡⟨ ≈-reflexive refl ⟨
  reverse (xs ∷ʳ x) ≈⟨ ≈-cong reverse (cast-reverse _ _) (unfold-∷ʳ (+-comm 1 n) x xs) ⟩
  reverse (xs ++ [ x ]) ≈⟨ reverse-++ (+-comm n 1) xs [ x ] ⟩
  x ∷ reverse xs ∎
@@ -249,6 +249,6 @@ example6b-reverse-∷ʳ-by-induction x (y ∷ xs) = begin
  reverse (y ∷ (xs ∷ʳ x)) ≡⟨ reverse-∷ y (xs ∷ʳ x) ⟩
  reverse (xs ∷ʳ x) ∷ʳ y ≡⟨ cong (_∷ʳ y) (example6b-reverse-∷ʳ-by-induction x xs) ⟩
  (x ∷ reverse xs) ∷ʳ y ≡⟨⟩
- x ∷ (reverse xs ∷ʳ y) ≡˘⟨ cong (x ∷_) (reverse-∷ y xs) ⟩
+ x ∷ (reverse xs ∷ʳ y) ≡⟨ cong (x ∷_) (reverse-∷ y xs) ⟨
  x ∷ reverse (y ∷ xs) ∎
  where open ≡-Reasoning

README/Tactic/Cong.agda

@@ -33,7 +33,7 @@ verbose-example m n eq =
  suc (suc m) + m
  ≡⟨ cong (λ ϕ → suc (suc (ϕ + ϕ))) eq ⟩
  suc (suc n) + n
- ≡˘⟨ cong (λ ϕ → suc (suc (n + ϕ))) (+-identityʳ n) ⟩
+ ≡⟨ cong (λ ϕ → suc (suc (n + ϕ))) (+-identityʳ n) ⟨
  suc (suc n) + (n + 0)
  ∎
 
@@ -51,7 +51,7 @@ succinct-example m n eq =
  suc (suc m) + m
  ≡⟨ cong! eq ⟩
  suc (suc n) + n
- ≡˘⟨ cong! (+-identityʳ n) ⟩
+ ≡⟨ cong! (+-identityʳ n) ⟨
  suc (suc n) + (n + 0)
  ∎
 
@@ -124,7 +124,7 @@ module EquationalReasoningTests where
  suc (suc m) + m
  ≡⟨ cong! eq ⟩
  suc (suc n) + n
- ≡˘⟨ cong! (+-identityʳ n) ⟩
+ ≡⟨ cong! (+-identityʳ n) ⟨
  suc (suc n) + (n + 0)
  ∎
 

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -56,11 +56,11 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
  y⁻¹*x⁻¹*x*y≈1 = begin
  y⁻¹ * x⁻¹ * (x * y - 0#) ≈⟨ *-congˡ (x-0≈x (x * y)) ⟩
  y⁻¹ * x⁻¹ * (x * y) ≈⟨ *-assoc y⁻¹ x⁻¹ (x * y) ⟩
- y⁻¹ * (x⁻¹ * (x * y)) ≈˘⟨ *-congˡ (*-assoc x⁻¹ x y) ⟩
- y⁻¹ * ((x⁻¹ * x) * y) ≈˘⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟩
+ y⁻¹ * (x⁻¹ * (x * y)) ≈⟨ *-congˡ (*-assoc x⁻¹ x y) ⟨
+ y⁻¹ * ((x⁻¹ * x) * y) ≈⟨ *-congˡ (*-congʳ (*-congˡ (x-0≈x x))) ⟨
  y⁻¹ * ((x⁻¹ * (x - 0#)) * y) ≈⟨ *-congˡ (*-congʳ x⁻¹*x≈1) ⟩
  y⁻¹ * (1# * y) ≈⟨ *-congˡ (*-identityˡ y) ⟩
- y⁻¹ * y ≈˘⟨ *-congˡ (x-0≈x y) ⟩
+ y⁻¹ * y ≈⟨ *-congˡ (x-0≈x y) ⟨
  y⁻¹ * (y - 0#) ≈⟨ y⁻¹*y≈1 ⟩
  1# ∎
 
@@ -75,15 +75,15 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
 
  y-x≈-[x-y] : y - x ≈ - (x - y)
  y-x≈-[x-y] = begin
- y - x ≈˘⟨ +-congʳ (-‿involutive y) ⟩
- - - y - x ≈˘⟨ -‿anti-homo-+ x (- y) ⟩
+ y - x ≈⟨ +-congʳ (-‿involutive y) ⟨
+ - - y - x ≈⟨ -‿anti-homo-+ x (- y) ⟨
  - (x - y) ∎
 
  x-y⁻¹*y-x≈1 : (- x-y⁻¹) * (y - x) ≈ 1#
  x-y⁻¹*y-x≈1 = begin
- (- x-y⁻¹) * (y - x) ≈˘⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟩
+ (- x-y⁻¹) * (y - x) ≈⟨ -‿distribˡ-* x-y⁻¹ (y - x) ⟨
  - (x-y⁻¹ * (y - x)) ≈⟨ -‿cong (*-congˡ y-x≈-[x-y]) ⟩
- - (x-y⁻¹ * - (x - y)) ≈˘⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟩
+ - (x-y⁻¹ * - (x - y)) ≈⟨ -‿cong (-‿distribʳ-* x-y⁻¹ (x - y)) ⟨
  - - (x-y⁻¹ * (x - y)) ≈⟨ -‿involutive (x-y⁻¹ * ((x - y))) ⟩
  x-y⁻¹ * (x - y) ≈⟨ InvX-Y .proj₂ .proj₁ ⟩
  1# ∎
@@ -100,7 +100,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
 
  x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
  x-z⁻¹*y-z≈1 = begin
- x-z⁻¹ * (y - z) ≈˘⟨ *-congˡ (+-congʳ x≈y) ⟩
+ x-z⁻¹ * (y - z) ≈⟨ *-congˡ (+-congʳ x≈y) ⟨
  x-z⁻¹ * (x - z) ≈⟨ x-z⁻¹*x-z≈1# ⟩
  1# ∎
 

src/Algebra/Consequences/Setoid.agda

@@ -88,7 +88,7 @@ module _ {f : Op₁ A} (self : SelfInverse f) where
 
  selfInverse⇒injective : Injective _≈_ _≈_ f
  selfInverse⇒injective {x} {y} x≈y = begin
- x ≈˘⟨ self x≈y ⟩
+ x ≈⟨ self x≈y ⟨
  f (f y) ≈⟨ selfInverse⇒involutive y ⟩
  y ∎
 
@@ -267,12 +267,12 @@ module _ {_•_ _◦_ : Op₂ A}
  _◦_ DistributesOver _•_ →
  _•_ DistributesOverˡ _◦_
  distrib+absorbs⇒distribˡ •-absorbs-◦ ◦-absorbs-• (◦-distribˡ-• , ◦-distribʳ-•) x y z = begin
- x • (y ◦ z) ≈˘⟨ •-cong (•-absorbs-◦ _ _) refl ⟩
+ x • (y ◦ z) ≈⟨ •-cong (•-absorbs-◦ _ _) refl ⟨
  (x • (x ◦ y)) • (y ◦ z) ≈⟨ •-cong (•-cong refl (◦-comm _ _)) refl ⟩
  (x • (y ◦ x)) • (y ◦ z) ≈⟨ •-assoc _ _ _ ⟩
- x • ((y ◦ x) • (y ◦ z)) ≈˘⟨ •-cong refl (◦-distribˡ-• _ _ _) ⟩
- x • (y ◦ (x • z)) ≈˘⟨ •-cong (◦-absorbs-• _ _) refl ⟩
- (x ◦ (x • z)) • (y ◦ (x • z)) ≈˘⟨ ◦-distribʳ-• _ _ _ ⟩
+ x • ((y ◦ x) • (y ◦ z)) ≈⟨ •-cong refl (◦-distribˡ-• _ _ _) ⟨
+ x • (y ◦ (x • z)) ≈⟨ •-cong (◦-absorbs-• _ _) refl ⟨
+ (x ◦ (x • z)) • (y ◦ (x • z)) ≈⟨ ◦-distribʳ-• _ _ _ ⟨
  (x • y) ◦ (x • z) ∎
 
 ------------------------------------------------------------------------

src/Algebra/Construct/LexProduct/Inner.agda

@@ -82,8 +82,8 @@ module NaturalOrder where
 
  ≤∙ˡ-trans : Associative _≈₁_ _∙_ → (a ∙ b) ≈₁ b → (b ∙ c) ≈₁ c → (a ∙ c) ≈₁ c
  ≤∙ˡ-trans {a} {b} {c} ∙-assoc ab≈b bc≈c = begin
- a ∙ c ≈˘⟨ ∙-congˡ bc≈c ⟩
- a ∙ (b ∙ c) ≈˘⟨ ∙-assoc a b c ⟩
+ a ∙ c ≈⟨ ∙-congˡ bc≈c ⟨
+ a ∙ (b ∙ c) ≈⟨ ∙-assoc a b c ⟨
  (a ∙ b) ∙ c ≈⟨ ∙-congʳ ab≈b ⟩
  b ∙ c ≈⟨ bc≈c ⟩
  c ∎
@@ -179,51 +179,51 @@ assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z
 ... | no ab≉a | yes ab≈b | yes bc≈b | yes bc≈c = begin
  lex (a ∙ b) c y z ≈⟨ cong₁ ab≈b ⟩
  lex b c y z ≈⟨ case₃ bc≈b bc≈c ⟩
- y ◦ z ≈˘⟨ case₂ ab≉a ab≈b ⟩
- lex a b x (y ◦ z) ≈˘⟨ cong₂ bc≈b ⟩
+ y ◦ z ≈⟨ case₂ ab≉a ab≈b ⟨
+ lex a b x (y ◦ z) ≈⟨ cong₂ bc≈b ⟨
  lex a (b ∙ c) x (y ◦ z) ∎
 ... | no ab≉a | yes ab≈b | yes bc≈b | no bc≉c = begin
  lex (a ∙ b) c y z ≈⟨ cong₁ ab≈b ⟩
  lex b c y z ≈⟨ case₁ bc≈b bc≉c ⟩
- y ≈˘⟨ case₂ ab≉a ab≈b ⟩
- lex a b x y ≈˘⟨ cong₂ bc≈b ⟩
+ y ≈⟨ case₂ ab≉a ab≈b ⟨
+ lex a b x y ≈⟨ cong₂ bc≈b ⟨
  lex a (b ∙ c) x y ∎
 ... | yes ab≈a | yes ab≈b | yes bc≈b | no bc≉c = begin
  lex (a ∙ b) c (x ◦ y) z ≈⟨ cong₁ ab≈b ⟩
  lex b c (x ◦ y) z ≈⟨ case₁ bc≈b bc≉c ⟩
- x ◦ y ≈˘⟨ case₃ ab≈a ab≈b ⟩
- lex a b x y ≈˘⟨ cong₂ bc≈b ⟩
+ x ◦ y ≈⟨ case₃ ab≈a ab≈b ⟨
+ lex a b x y ≈⟨ cong₂ bc≈b ⟨
  lex a (b ∙ c) x y ∎
 ... | yes ab≈a | yes ab≈b | yes bc≈b | yes bc≈c = begin
  lex (a ∙ b) c (x ◦ y) z ≈⟨ cong₁ ab≈b ⟩
  lex b c (x ◦ y) z ≈⟨ case₃ bc≈b bc≈c ⟩
  (x ◦ y) ◦ z ≈⟨ ◦-assoc x y z ⟩
- x ◦ (y ◦ z) ≈˘⟨ case₃ ab≈a ab≈b ⟩
- lex a b x (y ◦ z) ≈˘⟨ cong₂ bc≈b ⟩
+ x ◦ (y ◦ z) ≈⟨ case₃ ab≈a ab≈b ⟨
+ lex a b x (y ◦ z) ≈⟨ cong₂ bc≈b ⟨
  lex a (b ∙ c) x (y ◦ z) ∎
 ... | yes ab≈a | yes ab≈b | no bc≉b | yes bc≈c = begin
  lex (a ∙ b) c (x ◦ y) z ≈⟨ cong₁ ab≈b ⟩
  lex b c (x ◦ y) z ≈⟨ case₂ bc≉b bc≈c ⟩
- z ≈˘⟨ case₂ bc≉b bc≈c ⟩
- lex b c x z ≈˘⟨ cong₁₂ (M.trans (M.sym ab≈a) ab≈b) bc≈c ⟩
+ z ≈⟨ case₂ bc≉b bc≈c ⟨
+ lex b c x z ≈⟨ cong₁₂ (M.trans (M.sym ab≈a) ab≈b) bc≈c ⟨
  lex a (b ∙ c) x z ∎
 ... | yes ab≈a | no ab≉b | yes bc≈b | yes bc≈c = begin
  lex (a ∙ b) c x z ≈⟨ cong₁₂ ab≈a (M.trans (M.sym bc≈c) bc≈b) ⟩
  lex a b x z ≈⟨ case₁ ab≈a ab≉b ⟩
- x ≈˘⟨ case₁ ab≈a ab≉b ⟩
- lex a b x (y ◦ z) ≈˘⟨ cong₂ bc≈b ⟩
+ x ≈⟨ case₁ ab≈a ab≉b ⟨
+ lex a b x (y ◦ z) ≈⟨ cong₂ bc≈b ⟨
  lex a (b ∙ c) x (y ◦ z) ∎
 ... | no ab≉a | yes ab≈b | no bc≉b | yes bc≈c = begin
  lex (a ∙ b) c y z ≈⟨ cong₁ ab≈b ⟩
  lex b c y z ≈⟨ case₂ bc≉b bc≈c ⟩
- z ≈˘⟨ uncurry′ case₂ (<∙ˡ-trans ∙-assoc ∙-comm ab≈b ab≉a bc≈c) ⟩
- lex a c x z ≈˘⟨ cong₂ bc≈c ⟩
+ z ≈⟨ uncurry′ case₂ (<∙ˡ-trans ∙-assoc ∙-comm ab≈b ab≉a bc≈c) ⟨
+ lex a c x z ≈⟨ cong₂ bc≈c ⟨
  lex a (b ∙ c) x z ∎
 ... | yes ab≈a | no ab≉b | yes bc≈b | no bc≉c = begin
  lex (a ∙ b) c x z ≈⟨ cong₁ ab≈a ⟩
  lex a c x z ≈⟨ uncurry′ case₁ (<∙ʳ-trans ∙-assoc ∙-comm ab≈a bc≈b bc≉c) ⟩
- x ≈˘⟨ case₁ ab≈a ab≉b ⟩
- lex a b x y ≈˘⟨ cong₂ bc≈b ⟩
+ x ≈⟨ case₁ ab≈a ab≉b ⟨
+ lex a b x y ≈⟨ cong₂ bc≈b ⟨
  lex a (b ∙ c) x y ∎
 
 comm : Commutative _≈₁_ _∙_ → Commutative _≈₂_ _◦_ →