Construct proofs of 'basic' lattices

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

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
+    }

Lattice/Builder.agda

@@ -520,13 +520,13 @@ record Graph : Set where
         ⊥-is-⊥ : Is-⊥ ⊥
         ⊥-is-⊥ = foldr₁⊓-Suc nodes-nonempty
 
-        ⊔-refl : ∀ n → n ⊔ n ≡ n
+        ⊔-idemp : ∀ n → n ⊔ n ≡ n
-        ⊔-refl 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
+        ⊓-idemp : ∀ n → n ⊓ n ≡ n
-        ⊓-refl 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₂ → n₁ ⊔ (n₁ ⊓ n₂) ≡ n₁
-        ⊔-⊓-absorb 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₂ → n₁ ⊓ (n₁ ⊔ n₂) ≡ n₁
-        ⊓-⊔-absorb 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-⊓-⊔
+                }