From a083f2f4aed8dde2bd7d543a78af64dff6736561 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 14 Feb 2026 14:40:15 -0800
Subject: [PATCH] Construct proofs of 'basic' lattices

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Equivalence.agda     |  9 ++++++++-
 Lattice/Builder.agda | 41 +++++++++++++++++++++++++++++++++--------
 2 files changed, 41 insertions(+), 9 deletions(-)

diff --git a/Equivalence.agda b/Equivalence.agda
index c72631e..de9b004 100644
--- a/Equivalence.agda
+++ b/Equivalence.agda
@@ -2,7 +2,7 @@ module Equivalence where
 
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.Definitions
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
 
 module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
     IsReflexive : Set a
@@ -19,3 +19,10 @@ module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
             ≈-refl : IsReflexive
             ≈-sym : IsSymmetric
             ≈-trans : IsTransitive
+
+isEquivalence-≡ : ∀ {a} {A : Set a} → IsEquivalence A _≡_
+isEquivalence-≡ = record
+    { ≈-refl = refl
+    ; ≈-sym = sym
+    ; ≈-trans = trans
+    }
diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index cb80128..48a32ae 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -520,13 +520,13 @@ record Graph : Set where
         ⊥-is-⊥ : Is-⊥ ⊥
         ⊥-is-⊥ = foldr₁⊓-Suc nodes-nonempty
 
-        ⊔-refl : ∀ n → n ⊔ n ≡ n
-        ⊔-refl n
+        ⊔-idemp : ∀ n → n ⊔ n ≡ n
+        ⊔-idemp n
             with (n' , ((n'→n , _) , n''→n×n''→n⇒n''→n')) ← total-⊔ n n
             = n₁→n₂×n₂→n₁⇒n₁≡n₂ n'→n (n''→n×n''→n⇒n''→n' n (done , done))
 
-        ⊓-refl : ∀ n → n ⊓ n ≡ n
-        ⊓-refl n
+        ⊓-idemp : ∀ n → n ⊓ n ≡ n
+        ⊓-idemp n
             with (n' , ((n→n' , _) , n→n''×n→n''⇒n'→n'')) ← total-⊓ n n
             = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n→n''×n→n''⇒n'→n'' n (done , done)) n→n'
 
@@ -570,14 +570,39 @@ record Graph : Set where
                 n₁,₂₃→n₁₂,₃ = n₁→n'×n₂₃→n'⇒n₁,₂₃→n' n₁₂,₃ (n₁→n₁₂ ++ n₁₂→n₁₂,₃ , n₂₃→n₁₂,₃)
             in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃
 
-        ⊔-⊓-absorb : ∀ n₁ n₂ → n₁ ⊔ (n₁ ⊓ n₂) ≡ n₁
-        ⊔-⊓-absorb n₁ n₂
+        absorb-⊔-⊓ : ∀ n₁ n₂ → n₁ ⊔ (n₁ ⊓ n₂) ≡ n₁
+        absorb-⊔-⊓ n₁ n₂
             with (n₁₂ , ((n₁→n₁₂ , n₂→n₁₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
             with (n₁,₁₂ , ((n₁,₁₂→n₁ , n₁,₁₂→n₁₂) , n'→n₁×n'→n₁₂⇒n'→n₁,₁₂)) ← total-⊔ n₁ n₁₂
             = n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁,₁₂→n₁ (n'→n₁×n'→n₁₂⇒n'→n₁,₁₂ n₁ (done , n₁→n₁₂))
 
-        ⊓-⊔-absorb : ∀ n₁ n₂ → n₁ ⊓ (n₁ ⊔ n₂) ≡ n₁
-        ⊓-⊔-absorb n₁ n₂
+        absorb-⊓-⊔ : ∀ n₁ n₂ → n₁ ⊓ (n₁ ⊔ n₂) ≡ n₁
+        absorb-⊓-⊔ n₁ n₂
             with (n₁₂ , ((n₁₂→n₁ , n₁₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
             with (n₁,₁₂ , ((n₁→n₁,₁₂ , n₁₂→n₁,₁₂) , n₁→n'×n₁₂→n'⇒n₁,₁₂→n')) ← total-⊓ n₁ n₁₂
             = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₁₂→n'⇒n₁,₁₂→n' n₁ (done , n₁₂→n₁)) n₁→n₁,₁₂
+
+        instance
+            isJoinSemilattice : IsSemilattice Node _≡_ _⊔_
+            isJoinSemilattice = record
+                { ≈-equiv = isEquivalence-≡
+                ; ≈-⊔-cong = (λ { refl refl → refl })
+                ; ⊔-idemp = ⊔-idemp
+                ; ⊔-comm = ⊔-comm
+                ; ⊔-assoc = ⊔-assoc
+                }
+
+            isMeetSemilattice : IsSemilattice Node _≡_ _⊓_
+            isMeetSemilattice = record
+                { ≈-equiv = isEquivalence-≡
+                ; ≈-⊔-cong = (λ { refl refl → refl })
+                ; ⊔-idemp = ⊓-idemp
+                ; ⊔-comm = ⊓-comm
+                ; ⊔-assoc = ⊓-assoc
+                }
+
+            isLattice : IsLattice Node _≡_ _⊔_ _⊓_
+            isLattice = record
+                { absorb-⊔-⊓ = absorb-⊔-⊓
+                ; absorb-⊓-⊔ = absorb-⊓-⊔
+                }