Simplify inequality reasoning syntax in posets (#1533)

Pulled from #1353 .

Author: lowasser

src/order-theory/join-semilattices.lagda.md

@@ -497,28 +497,28 @@ module _
   leq-left-triple-join-Order-Theoretic-Join-Semilattice :
     x ≤ ((x ∨ y) ∨ z)
   leq-left-triple-join-Order-Theoretic-Join-Semilattice =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Join-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Join-Semilattice A)
+    in
       chain-of-inequalities
         x ≤ x ∨ y
             by leq-left-join-Order-Theoretic-Join-Semilattice A x y
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
           ≤ (x ∨ y) ∨ z
             by leq-left-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
 
   leq-center-triple-join-Order-Theoretic-Join-Semilattice :
     y ≤ ((x ∨ y) ∨ z)
   leq-center-triple-join-Order-Theoretic-Join-Semilattice =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Join-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Join-Semilattice A)
+    in
       chain-of-inequalities
         y ≤ x ∨ y
             by leq-right-join-Order-Theoretic-Join-Semilattice A x y
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
           ≤ (x ∨ y) ∨ z
             by leq-left-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
 
   leq-right-triple-join-Order-Theoretic-Join-Semilattice :
     z ≤ ((x ∨ y) ∨ z)
@@ -533,28 +533,28 @@ module _
   leq-center-triple-join-Order-Theoretic-Join-Semilattice' :
     y ≤ (x ∨ (y ∨ z))
   leq-center-triple-join-Order-Theoretic-Join-Semilattice' =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Join-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Join-Semilattice A)
+    in
       chain-of-inequalities
         y ≤ y ∨ z
             by leq-left-join-Order-Theoretic-Join-Semilattice A y z
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
           ≤ x ∨ (y ∨ z)
             by leq-right-join-Order-Theoretic-Join-Semilattice A x (y ∨ z)
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
 
   leq-right-triple-join-Order-Theoretic-Join-Semilattice' :
     z ≤ (x ∨ (y ∨ z))
   leq-right-triple-join-Order-Theoretic-Join-Semilattice' =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Join-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Join-Semilattice A)
+    in
       chain-of-inequalities
         z ≤ y ∨ z
             by leq-right-join-Order-Theoretic-Join-Semilattice A y z
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
           ≤ x ∨ (y ∨ z)
             by leq-right-join-Order-Theoretic-Join-Semilattice A x (y ∨ z)
-            in-Poset poset-Order-Theoretic-Join-Semilattice A
 
   leq-associative-join-Order-Theoretic-Join-Semilattice :
     ((x ∨ y) ∨ z) ≤ (x ∨ (y ∨ z))

src/order-theory/meet-semilattices.lagda.md

@@ -503,30 +503,30 @@ module _
   leq-left-triple-meet-Order-Theoretic-Meet-Semilattice :
     ((x ∧ y) ∧ z) ≤ x
   leq-left-triple-meet-Order-Theoretic-Meet-Semilattice =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Meet-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Meet-Semilattice A)
+    in
       chain-of-inequalities
         (x ∧ y) ∧ z
           ≤ x ∧ y
             by leq-left-meet-Order-Theoretic-Meet-Semilattice A (x ∧ y) z
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
           ≤ x
             by leq-left-meet-Order-Theoretic-Meet-Semilattice A x y
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
 
   leq-center-triple-meet-Order-Theoretic-Meet-Semilattice :
     ((x ∧ y) ∧ z) ≤ y
   leq-center-triple-meet-Order-Theoretic-Meet-Semilattice =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Meet-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Meet-Semilattice A)
+    in
       chain-of-inequalities
         (x ∧ y) ∧ z
           ≤ x ∧ y
             by leq-left-meet-Order-Theoretic-Meet-Semilattice A (x ∧ y) z
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
           ≤ y
             by leq-right-meet-Order-Theoretic-Meet-Semilattice A x y
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
 
   leq-right-triple-meet-Order-Theoretic-Meet-Semilattice :
     ((x ∧ y) ∧ z) ≤ z
@@ -541,30 +541,30 @@ module _
   leq-center-triple-meet-Order-Theoretic-Meet-Semilattice' :
     (x ∧ (y ∧ z)) ≤ y
   leq-center-triple-meet-Order-Theoretic-Meet-Semilattice' =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Meet-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Meet-Semilattice A)
+    in
       chain-of-inequalities
         x ∧ (y ∧ z)
           ≤ y ∧ z
             by leq-right-meet-Order-Theoretic-Meet-Semilattice A x (y ∧ z)
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
           ≤ y
             by leq-left-meet-Order-Theoretic-Meet-Semilattice A y z
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
 
   leq-right-triple-meet-Order-Theoretic-Meet-Semilattice' :
     (x ∧ (y ∧ z)) ≤ z
   leq-right-triple-meet-Order-Theoretic-Meet-Semilattice' =
-    calculate-in-Poset
-      ( poset-Order-Theoretic-Meet-Semilattice A)
+    let
+      open
+        inequality-reasoning-Poset (poset-Order-Theoretic-Meet-Semilattice A)
+    in
       chain-of-inequalities
         x ∧ (y ∧ z)
           ≤ y ∧ z
             by leq-right-meet-Order-Theoretic-Meet-Semilattice A x (y ∧ z)
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
           ≤ z
             by leq-right-meet-Order-Theoretic-Meet-Semilattice A y z
-            in-Poset poset-Order-Theoretic-Meet-Semilattice A
 
   leq-associative-meet-Order-Theoretic-Meet-Semilattice :
     ((x ∧ y) ∧ z) ≤ (x ∧ (y ∧ z))

src/order-theory/posets.lagda.md

@@ -121,38 +121,37 @@ module _
 Inequalities in preorders can be constructed by equational reasoning as follows:
 
 ```text
-calculate-in-Poset X
+let open inequality-reasoning-Poset X
+in
   chain-of-inequalities
   x ≤ y
       by ineq-1
-      in-Poset X
     ≤ z
       by ineq-2
-      in-Poset X
     ≤ v
       by ineq-3
-      in-Poset X
 ```
 
 Note, however, that in our setup of equational reasoning with inequalities it is
 not possible to mix inequalities with equalities or strict inequalities.
 
 ```agda
-infixl 1 calculate-in-Poset_chain-of-inequalities_
-infixl 0 step-calculate-in-Poset
-
-calculate-in-Poset_chain-of-inequalities_ :
+module inequality-reasoning-Poset
   {l1 l2 : Level} (X : Poset l1 l2)
-  (x : type-Poset X) → leq-Poset X x x
-calculate-in-Poset_chain-of-inequalities_ = refl-leq-Poset
+  where
 
-step-calculate-in-Poset :
-  {l1 l2 : Level} (X : Poset l1 l2)
-  {x y : type-Poset X} → leq-Poset X x y →
-  (z : type-Poset X) → leq-Poset X y z → leq-Poset X x z
-step-calculate-in-Poset X {x} {y} u z v = transitive-leq-Poset X x y z v u
+  infixl 1 chain-of-inequalities_
+  infixl 0 step-calculate-in-Poset
+
+  chain-of-inequalities_ : (x : type-Poset X) → leq-Poset X x x
+  chain-of-inequalities_ = refl-leq-Poset X
+
+  step-calculate-in-Poset :
+    {x y : type-Poset X} → leq-Poset X x y →
+    (z : type-Poset X) → leq-Poset X y z → leq-Poset X x z
+  step-calculate-in-Poset {x} {y} u z v = transitive-leq-Poset X x y z v u
 
-syntax step-calculate-in-Poset X u z v = u ≤ z by v in-Poset X
+  syntax step-calculate-in-Poset u z v = u ≤ z by v
 ```
 
 ## Properties
@@ -201,3 +200,17 @@ module _
 ```
 
 It remains to show that these constructions form inverses to each other.
+
+### 3-cycles in poset inequalities
+
+```agda
+abstract
+  three-cycle-leq-Poset :
+    {l1 l2 : Level} → (P : Poset l1 l2) → {a b c : type-Poset P} →
+    leq-Poset P a b → leq-Poset P b c → leq-Poset P c a →
+    (a ＝ b) × (a ＝ c) × (b ＝ c)
+  three-cycle-leq-Poset P {a} {b} {c} a≤b b≤c c≤a =
+    ( antisymmetric-leq-Poset P a b a≤b (transitive-leq-Poset P _ c _ c≤a b≤c) ,
+      antisymmetric-leq-Poset P a c (transitive-leq-Poset P _ b _ b≤c a≤b) c≤a ,
+      antisymmetric-leq-Poset P b c b≤c (transitive-leq-Poset P _ a _ a≤b c≤a))
+```