[WIP] Demonstrate partial lattice construction

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

Lattice/Builder.agda

@@ -217,6 +217,7 @@ record PartialLattice {a} (A : Set a) : Set (lsuc a) where
     least-⊔-identˡ le x = ≈?-trans (⊔-comm (HasLeastElement.x le) x) (least-⊔-identʳ le x)
 
 record PartialLatticeType (a : Level) : Set (lsuc a) where
+    constructor mkPartialLatticeType
     field
         EltType : Set a
         {{partialLattice}} : PartialLattice EltType
@@ -1139,6 +1140,59 @@ instance
             ; ≈-⊔-cong = ≈-⊓̇-cong {Ls = Ls}
             }
 
+⊔̇-⊓̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+⊔̇-⊓̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathJoin' Ls) (pathMeet' Ls)
+                                   (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+                                   (λ _ _ → refl) (λ _ _ → refl)
+                                   (absorb-pathJoin'-pathMeet' {Ls = Ls}) p₁ p₂
+
+⊓̇-⊔̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+⊓̇-⊔̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
+    = PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathMeet' Ls) (pathJoin' Ls)
+                                   (_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
+                                   (λ _ _ → refl) (λ _ _ → refl)
+                                   (absorb-pathMeet'-pathJoin' {Ls = Ls}) p₁ p₂
+
+instance
+    Path-IsPartialLattice : ∀ {a} {Ls : Layers a} → IsPartialLattice (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
+    Path-IsPartialLattice {Ls = Ls} =
+        record
+            { absorb-⊔-⊓ = ⊔̇-⊓̇-absorb {Ls = Ls}
+            ; absorb-⊓-⊔ = ⊓̇-⊔̇-absorb {Ls = Ls}
+            }
+
+instance
+    -- IsLattice-IsPartialLattice : ∀ {a} {A : Set a}
+    --     {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A}
+    --     {{lA : IsLattice A _≈_ _⊔_ _⊓_}} → IsPartialLattice _≈_ _⊔_ _⊓_
+    -- IsLattice-IsPartialLattice = {!!}
+
+    Lattice-PartialLattice : ∀ {a} {A : Set a}
+        {{lA : Lattice A }} →  PartialLattice A
+    Lattice-PartialLattice = {!!}
+
+    Lattice-Least : ∀ {a} {A : Set a}
+        {{lA : Lattice A }} → PartialLattice.HasLeastElement (Lattice-PartialLattice {{lA = lA}})
+    Lattice-Least = {!!}
+
+open import Lattice.Unit
+
+ThreeElements : Set
+ThreeElements = Path (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (single ((mkPartialLatticeType ⊤) ∷⁺ []))))
+
+e₁ : ThreeElements
+e₁ = MkPath (inj₁ (inj₁ tt))
+
+e₂ : ThreeElements
+e₂ = MkPath (inj₂ (inj₁ (inj₁ tt)))
+
+e₃ : ThreeElements
+e₃ = MkPath (inj₂ (inj₂ (inj₁ tt)))
+
+ex1 : e₁ ⊔̇ e₂ ≡ just e₁
+ex1 = refl
+
 -- 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)