refactor(McBride): small cleanup

RedPRL · Dec 1, 2023 · f31bc60 · f31bc60
1 parent b65f1bd
commit f31bc60
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/Mugen/Cat/HierarchyTheory/McBride.agda b/src/Mugen/Cat/HierarchyTheory/McBride.agda
@@ -71,11 +71,9 @@ import Mugen.Order.Reasoning
 
           d2≤d1 : d2 ≤ d1
           d2≤d1 =
-            d2      ≐⟨ sym idr ⟩
-            d2 ⊗ ε  ≤⟨ left-invariant ε≤e2 ⟩
+            d2      ≤⟨ d2≤d2⊗e2 ⟩
             d2 ⊗ e2 ≐⟨ sym $ ap snd p ⟩
-            d1 ⊗ e1 ≤⟨ left-invariant e1≤ε ⟩
-            d1 ⊗ ε  ≐⟨ idr ⟩
+            d1 ⊗ e1 ≤⟨ d1⊗e1≤d1 ⟩
             d1      ≤∎
 
           d1=d2 : d1 ≡ d2