From 28087593388e75b7c51d92e117f986bbbed778f5 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 25 Jul 2025 17:18:19 +0200
Subject: [PATCH] Add instances of semilattice proofs

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Builder.agda | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 44ead6d..d008f2c 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -72,7 +72,7 @@ record IsPartialSemilattice {a} {A : Set a}
     _≼_ x y = (x ⊔? y) ≈? (just y)
 
     field
-        ≈-equiv : IsEquivalence A _≈_
+        {{≈-equiv}} : IsEquivalence A _≈_
         ≈-⊔-cong : PartialCong _≈_ _⊔?_
 
         ⊔-assoc : PartialAssoc _≈_ _⊔?_
@@ -1010,6 +1010,25 @@ _⊓̇_-idemp {Ls = Ls} (MkPath p)
 ≈-⊓̇-cong {Ls = Ls} (mk-≈ p₁≈p₂) (mk-≈ p₃≈p₄) =
     lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (eqPath'-pathMeet'-cong {Ls = Ls} p₁≈p₂ p₃≈p₄)
 
+instance
+    Path-IsPartialJoinSemilattice : ∀ {a} {Ls : Layers a} → IsPartialSemilattice (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+    Path-IsPartialJoinSemilattice {Ls = Ls} =
+        record
+            { ⊔-assoc = _⊔̇_-assoc {Ls = Ls}
+            ; ⊔-comm = _⊔̇_-comm {Ls = Ls}
+            ; ⊔-idemp = _⊔̇_-idemp {Ls = Ls}
+            ; ≈-⊔-cong = ≈-⊔̇-cong {Ls = Ls}
+            }
+
+    Path-IsPartialMeetSemilattice : ∀ {a} {Ls : Layers a} → IsPartialSemilattice (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+    Path-IsPartialMeetSemilattice {Ls = Ls} =
+        record
+            { ⊔-assoc = _⊓̇_-assoc {Ls = Ls}
+            ; ⊔-comm = _⊓̇_-comm {Ls = Ls}
+            ; ⊔-idemp = _⊓̇_-idemp {Ls = Ls}
+            ; ≈-⊔-cong = ≈-⊓̇-cong {Ls = Ls}
+            }
+
 -- data ListValue {a : Level} : List (PartialLatticeType a) → Set (lsuc a) where
 --     here : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)}
 --              (v : PartialLatticeType.EltType plt) → ListValue (plt ∷ pltl)