From 8febffc8e3901821c583bece6bc19ae144fee44c Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 15 Jul 2023 15:16:51 -0700
Subject: [PATCH] Add an equivalence constraint on lattice relations.

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

diff --git a/Lattice.agda b/Lattice.agda
index 1873547..eaaa0a6 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -1,7 +1,7 @@
 module Lattice where
 
 import Data.Nat.Properties as NatProps
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; isEquivalence)
 open import Relation.Binary.Definitions
 open import Data.Nat as Nat using (ℕ; _≤_)
 open import Data.Product using (_×_; _,_)
@@ -10,15 +10,25 @@ open import Agda.Primitive using (lsuc; Level)
 
 open import NatMap using (NatMap)
 
+record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
+    field
+        ≈-refl : {a : A} → a ≈ a
+        ≈-sym : {a b : A} → a ≈ b → b ≈ a
+        ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c
+
 record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where
 
     field
+        ≈-equiv : IsEquivalence A _≈_
+
         ⊔-assoc : (x y z : A) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
         ⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
         ⊔-idemp : (x : A) → (x ⊔ x) ≈ x
 
+    open IsEquivalence ≈-equiv public
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)
@@ -66,14 +76,24 @@ module IsSemilatticeInstances where
 
         NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
         NatIsMaxSemilattice = record
-            { ⊔-assoc = ⊔-assoc
+            { ≈-equiv = record
+                { ≈-refl = refl
+                ; ≈-sym = sym
+                ; ≈-trans = trans
+                }
+            ; ⊔-assoc = ⊔-assoc
             ; ⊔-comm = ⊔-comm
             ; ⊔-idemp = ⊔-idem
             }
 
         NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
         NatIsMinSemilattice = record
-            { ⊔-assoc = ⊓-assoc
+            { ≈-equiv = record
+                { ≈-refl = refl
+                ; ≈-sym = sym
+                ; ≈-trans = trans
+                }
+            ; ⊔-assoc = ⊓-assoc
             ; ⊔-comm = ⊓-comm
             ; ⊔-idemp = ⊓-idem
             }
@@ -114,9 +134,33 @@ module IsSemilatticeInstances where
                 , IsSemilattice.⊔-idemp sB b
                 )
 
+            ≈-refl : {p : A × B} → p ≈ p
+            ≈-refl =
+                ( IsSemilattice.≈-refl sA
+                , IsSemilattice.≈-refl sB
+                )
+
+            ≈-sym : {p₁ p₂ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₁
+            ≈-sym (a₁≈a₂ , b₁≈b₂) =
+                ( IsSemilattice.≈-sym sA a₁≈a₂
+                , IsSemilattice.≈-sym sB b₁≈b₂
+                )
+
+            ≈-trans : {p₁ p₂ p₃ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₃ → p₁ ≈ p₃
+            ≈-trans (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) =
+                ( IsSemilattice.≈-trans sA a₁≈a₂ a₂≈a₃
+                , IsSemilattice.≈-trans sB b₁≈b₂ b₂≈b₃
+                )
+
+
         ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
         ProdIsSemilattice = record
-            { ⊔-assoc = ⊔-assoc
+            { ≈-equiv = record
+                { ≈-refl = ≈-refl
+                ; ≈-sym = ≈-sym
+                ; ≈-trans = ≈-trans
+                }
+            ; ⊔-assoc = ⊔-assoc
             ; ⊔-comm = ⊔-comm
             ; ⊔-idemp = ⊔-idemp
             }