From c9b514e9af35a5af5d8128b9b1ba06a7d1e55d9c Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 14 Jul 2023 19:42:29 -0700
Subject: [PATCH] Add a preorder instance for product

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice.agda | 59 ++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 48 insertions(+), 11 deletions(-)

diff --git a/Lattice.agda b/Lattice.agda
index b6c61d8..5589629 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -85,21 +85,58 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
 
     open IsLattice isLattice public
 
+module PreorderInstances where
+    module ForNat where
+        open NatProps
+
+        NatPreorder : Preorder ℕ
+        NatPreorder = record
+            { _≼_ = _≤_
+            ; isPreorder = record
+                { ≼-refl = ≤-refl
+                ; ≼-trans = ≤-trans
+                ; ≼-antisym = ≤-antisym
+                }
+            }
+
+    module ForProd {a} {A B : Set a} {{ pA : Preorder A }} {{ pB : Preorder B }} where
+        open Eq
+
+        private
+            _≼_ : A × B → A × B → Set a
+            (a₁ ,  b₁) ≼ (a₂ , b₂) = Preorder._≼_ pA a₁ a₂ × Preorder._≼_ pB b₁ b₂
+
+            ispA = Preorder.isPreorder pA
+            ispB = Preorder.isPreorder pB
+
+            ≼-refl : {p : A × B} → p ≼ p
+            ≼-refl {(a , b)} = (IsPreorder.≼-refl ispA {a}, IsPreorder.≼-refl ispB {b})
+
+            ≼-trans : {p₁ p₂ p₃ : A × B} → p₁ ≼ p₂ → p₂ ≼ p₃ → p₁ ≼ p₃
+            ≼-trans (a₁≼a₂ , b₁≼b₂) (a₂≼a₃ , b₂≼b₃) =
+                ( IsPreorder.≼-trans ispA a₁≼a₂ a₂≼a₃
+                , IsPreorder.≼-trans ispB b₁≼b₂ b₂≼b₃
+                )
+
+            ≼-antisym : {p₁ p₂ : A × B} → p₁ ≼ p₂ → p₂ ≼ p₁ → p₁ ≡ p₂
+            ≼-antisym (a₁≼a₂ , b₁≼b₂) (a₂≼a₁ , b₂≼b₁) = cong₂ (_,_) (IsPreorder.≼-antisym ispA a₁≼a₂ a₂≼a₁) (IsPreorder.≼-antisym ispB b₁≼b₂ b₂≼b₁)
+
+        ProdPreorder : Preorder (A × B)
+        ProdPreorder = record
+            { _≼_ = _≼_
+            ; isPreorder = record
+                { ≼-refl = ≼-refl
+                ; ≼-trans = ≼-trans
+                ; ≼-antisym = ≼-antisym
+                }
+            }
+
+
 private module NatInstances where
     open Nat
     open NatProps
     open Eq
-    open Data.Sum
-
-    NatPreorder : Preorder ℕ
-    NatPreorder = record
-        { _≼_ = _≤_
-        ; isPreorder = record
-            { ≼-refl = ≤-refl
-            ; ≼-trans = ≤-trans
-            ; ≼-antisym = ≤-antisym
-            }
-        }
+    open PreorderInstances.ForNat
 
     private
         max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z