module Lattice.Builder where

open import Lattice
open import Equivalence
open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
open import Data.Unit using (⊤; tt)
open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
open import Data.List using (List; _∷_; [])
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _,_)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)

maybe-injection : ∀ {a} {A : Set a} (x : A) → just x ≡ nothing → ⊥
maybe-injection x ()

data lift-≈ {a} {A : Set a} (_≈_ : A → A → Set a) : Maybe A → Maybe A → Set a where
    ≈-just : ∀ {a₁ a₂ : A} →  a₁ ≈ a₂ →  lift-≈ _≈_ (just a₁) (just a₂)
    ≈-nothing : lift-≈ _≈_ nothing nothing

lift-≈-map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B)
               (_≈ᵃ_ : A → A → Set a) (_≈ᵇ_ : B → B → Set b) →
               (∀ a₁ a₂ → a₁ ≈ᵃ a₂ → f a₁ ≈ᵇ f a₂) →
               ∀ m₁ m₂ → lift-≈ _≈ᵃ_ m₁ m₂ → lift-≈ _≈ᵇ_ (Maybe.map f m₁) (Maybe.map f m₂)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ (just a₁) (just a₂) (≈-just a₁≈a₂) = ≈-just (≈ᵃ→≈ᵇ a₁ a₂ a₁≈a₂)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ nothing nothing ≈-nothing = ≈-nothing

instance
    lift-≈-Equivalence : ∀ {a} {A : Set a} {_≈_ : A → A → Set a} {{isEquivalence : IsEquivalence A _≈_}} → IsEquivalence (Maybe A) (lift-≈ _≈_)
    lift-≈-Equivalence {{isEquivalence}} = record
        { ≈-trans =
            (λ { (≈-just a₁≈a₂) (≈-just a₂≈a₃) → ≈-just (IsEquivalence.≈-trans isEquivalence a₁≈a₂ a₂≈a₃)
               ; ≈-nothing ≈-nothing → ≈-nothing
               })
        ; ≈-sym =
            (λ { (≈-just a₁≈a₂) → ≈-just (IsEquivalence.≈-sym isEquivalence a₁≈a₂)
               ; ≈-nothing → ≈-nothing
               })
        ; ≈-refl = λ { {just a} → ≈-just (IsEquivalence.≈-refl isEquivalence)
                     ; {nothing} → ≈-nothing
                     }
        }

PartialAssoc : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialAssoc {a} {A} _≈_ _⊗_ = ∀ (x y z : A) →  lift-≈ _≈_ ((x ⊗ y) >>= (_⊗ z)) ((y ⊗ z) >>= (x ⊗_))

PartialComm : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialComm {a} {A} _≈_ _⊗_ = ∀ (x y : A) →  lift-≈ _≈_ (x ⊗ y) (y ⊗ x)

PartialIdemp : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialIdemp {a} {A} _≈_ _⊗_ = ∀ (x : A) →  lift-≈ _≈_ (x ⊗ x) (just x)

data Trivial a : Set a where
    instance
        mkTrivial : Trivial a

data Empty a : Set a where

record IsPartialSemilattice {a} {A : Set a}
    (_≈_ : A → A → Set a)
    (_⊔?_ : A → A → Maybe A) : Set a where

    _≈?_ : Maybe A → Maybe A → Set a
    _≈?_ = lift-≈ _≈_

    _≼_ : A → A → Set a
    _≼_ x y = (x ⊔? y) ≈? (just y)

    field
        ≈-equiv : IsEquivalence A _≈_
        ≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔? a₃) ≈? (a₂ ⊔? a₄)

        ⊔-assoc : PartialAssoc _≈_ _⊔?_
        ⊔-comm : PartialComm _≈_ _⊔?_
        ⊔-idemp : PartialIdemp _≈_ _⊔?_

    open IsEquivalence ≈-equiv public
    open IsEquivalence (lift-≈-Equivalence {{≈-equiv}}) public using ()
        renaming (≈-trans to ≈?-trans; ≈-sym to ≈?-sym; ≈-refl to ≈?-refl)

    ≈-≼-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ →  a₁ ≼ a₃ → a₂ ≼ a₄
    ≈-≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁≼a₃ = ≈?-trans (≈?-trans (≈?-sym (≈-⊔-cong a₁≈a₂ a₃≈a₄)) a₁≼a₃) (≈-just a₃≈a₄)

    -- curious: similar property (properties?) to partial commutative monoids (PCMs)
    -- from Iris.
    ≼-partialˡ : ∀ {a a₁ a₂} → a₁ ≼ a₂ →  (a ⊔? a₁) ≡ nothing → (a ⊔? a₂) ≡ nothing
    ≼-partialˡ {a} {a₁} {a₂} a₁≼a₂ a⊔a₁≡nothing
        with a₁ ⊔? a₂ | a₁≼a₂ | a ⊔? a₁ | a⊔a₁≡nothing | ⊔-assoc a a₁ a₂
    ...   | just a₁⊔a₂ | ≈-just a₁⊔a₂≈a₂ | nothing | refl | aa₁⊔a₂≈a⊔a₁a₂
            with a ⊔? a₁⊔a₂ | aa₁⊔a₂≈a⊔a₁a₂ | a ⊔? a₂ | ≈-⊔-cong (≈-refl {a = a}) a₁⊔a₂≈a₂
    ...       | nothing | ≈-nothing | nothing | ≈-nothing = refl

    ≼-partialʳ : ∀ {a a₁ a₂} → a₁ ≼ a₂ →  (a₁ ⊔? a) ≡ nothing → (a₂ ⊔? a) ≡ nothing
    ≼-partialʳ {a} {a₁} {a₂} a₁≼a₂ a₁⊔a≡nothing
        with a₁ ⊔? a | a ⊔? a₁ | a₁⊔a≡nothing | ⊔-comm a₁ a | ≼-partialˡ {a} {a₁} {a₂} a₁≼a₂
    ...   | nothing | nothing | refl | ≈-nothing | refl⇒a⊔a₂=nothing
            with a₂ ⊔? a | a ⊔? a₂ | ⊔-comm a₂ a | refl⇒a⊔a₂=nothing refl
    ...       | nothing | nothing | ≈-nothing | refl = refl

    ≼-refl : ∀ (x : A) →  x ≼ x
    ≼-refl x = ⊔-idemp x

    ≼-refl' : ∀ {a₁ a₂ : A} → a₁ ≈ a₂ → a₁ ≼ a₂
    ≼-refl' {a₁} {a₂} a₁≈a₂ = ≈-≼-cong ≈-refl a₁≈a₂ (≼-refl a₁)

    x⊔?x≼x : ∀ (x : A) →  maybe (λ x⊔x →  x⊔x ≼ x) (Empty a) (x ⊔? x)
    x⊔?x≼x x
        with x ⊔? x | ⊔-idemp x
    ...   | just x⊔x | ≈-just x⊔x≈x = ≈-≼-cong (≈-sym x⊔x≈x) ≈-refl (≼-refl x)

    x≼x⊔?y : ∀ (x y : A) →  maybe (λ x⊔y →  x ≼ x⊔y) (Trivial a) (x ⊔? y)
    x≼x⊔?y x y
        with x ⊔? y in x⊔?y= | x ⊔? x | ⊔-idemp x | ⊔-assoc x x y | x⊔?x≼x x
    ...   | nothing  | _ | _ | _ | _ = mkTrivial
    ...   | just x⊔y | just x⊔x | ≈-just x⊔x≈x | ⊔-assoc-xxy | x⊔x≼x
            with x⊔x ⊔? y in xx⊔?y= | x ⊔? x⊔y
    ...       | nothing | nothing =
                ⊥-elim (maybe-injection _ (trans (sym x⊔?y=) (≼-partialʳ x⊔x≼x xx⊔?y=)))
    ...       | just xx⊔y | just x⊔xy rewrite (sym xx⊔?y=) rewrite (sym x⊔?y=) =
                ≈?-trans (≈?-sym ⊔-assoc-xxy) (≈-⊔-cong x⊔x≈x (≈-refl {a = y}))

    record HasIdentityElement : Set a where
        field
            x : A
            not-partial : ∀ (a₁ a₂ : A) →  Σ A (λ a₃ →  (a₁ ⊔? a₂) ≡ just a₃)
            x-identityˡ : (a : A) → (x ⊔? a) ≈? just a

        x-identityʳ : (a : A) → (a ⊔? x) ≈? just a
        x-identityʳ a = ≈?-trans (⊔-comm a x) (x-identityˡ a)

record IsPartialLattice {a} {A : Set a}
    (_≈_ : A → A → Set a)
    (_⊔?_ : A → A → Maybe A)
    (_⊓?_ : A → A → Maybe A) : Set a where

    field
        {{partialJoinSemilattice}} : IsPartialSemilattice _≈_ _⊔?_
        {{partialMeetSemilattice}} : IsPartialSemilattice _≈_ _⊓?_

        absorb-⊔-⊓ : (x y : A) →  maybe (λ x⊓y → lift-≈ _≈_ (x ⊔? x⊓y) (just x)) (Trivial _) (x ⊓? y)
        absorb-⊓-⊔ : (x y : A) →  maybe (λ x⊔y → lift-≈ _≈_ (x ⊓? x⊔y) (just x)) (Trivial _) (x ⊔? y)

    open IsPartialSemilattice partialJoinSemilattice public
    open IsPartialSemilattice partialMeetSemilattice using ()
        renaming
            ( ≈-⊔-cong to ≈-⊓-cong
            ; ⊔-assoc to ⊓-assoc
            ; ⊔-comm to ⊓-comm
            ; ⊔-idemp to ⊓-idemp
            )
        public

record PartialLattice {a} (A : Set a) : Set (lsuc a) where
    field
        _≈_ : A → A → Set a
        _⊔?_ : A → A → Maybe A
        _⊓?_ : A → A → Maybe A

        {{isPartialLattice}} : IsPartialLattice _≈_ _⊔?_ _⊓?_

    open IsPartialLattice isPartialLattice public

    HasLeastElement : Set a
    HasLeastElement =
        IsPartialSemilattice.HasIdentityElement
            (IsPartialLattice.partialJoinSemilattice isPartialLattice)

    HasGreatestElement : Set a
    HasGreatestElement =
        IsPartialSemilattice.HasIdentityElement
            (IsPartialLattice.partialMeetSemilattice isPartialLattice)

record PartialLatticeType (a : Level) : Set (lsuc a) where
    field
        EltType : Set a
        {{partialLattice}} : PartialLattice EltType

    open PartialLattice partialLattice public

Layer : (a : Level) → Set (lsuc a)
Layer a = List⁺ (PartialLatticeType a)

data LayerLeast {a} : Layer a → Set (lsuc a) where
    instance
        MkLayerLeast : {T : Set a}
                       {{ partialLattice : PartialLattice T }}
                       {{ hasLeast : PartialLattice.HasLeastElement partialLattice }} →
                       LayerLeast (record { EltType = T; partialLattice = partialLattice } ∷⁺ [])

data LayerGreatest {a} : Layer a → Set (lsuc a) where
    instance
        MkLayerGreatest : {T : Set a}
                       {{ partialLattice : PartialLattice T }}
                       {{ hasGreatest : PartialLattice.HasGreatestElement partialLattice }} →
                       LayerGreatest (record { EltType = T; partialLattice = partialLattice } ∷⁺ [])

interleaved mutual
    data Layers a : Set (lsuc a)
    head : ∀ {a} → Layers a → Layer a

    data Layers where
        single : Layer a → Layers a
        add-via-least : (l : Layer a) {{ least : LayerLeast l }} (ls : Layers a) → Layers a
        add-via-greatest : (l : Layer a) (ls : Layers a) {{ greatest : LayerGreatest (head ls) }} → Layers a

    head (single l) = l
    head (add-via-greatest l _) = l
    head (add-via-least l _) = l

ListValue : ∀ {a} → List (PartialLatticeType a) → Set a
ListValue [] = Empty _
ListValue (plt ∷ plts) = PartialLatticeType.EltType plt ⊎ ListValue plts

-- Define LayerValue and Path' as functions to avoid increasing the universe level.
-- Path' in particular needs to be at the same level as the other lattices
-- in the builder to ensure composability.

LayerValue : ∀ {a} →  Layer a → Set a
LayerValue l⁺ = ListValue (toList l⁺)

Path' : ∀ {a} → Layers a → Set a
Path' (single l) = LayerValue l
Path' (add-via-least l ls) = LayerValue l ⊎ Path' ls
Path' (add-via-greatest l ls) = LayerValue l ⊎ Path' ls

record Path {a} (Ls : Layers a) : Set a where
    constructor MkPath
    field path : Path' Ls

valueAtHead : ∀ {a} (ls : Layers a) (lv : LayerValue (head ls)) → Path' ls
valueAtHead (single _) lv = lv
valueAtHead (add-via-least _ _) lv = inj₁ lv
valueAtHead (add-via-greatest _ _) lv = inj₁ lv

CombineForPLT : ∀ a → Set (lsuc a)
CombineForPLT a = ∀ (plt : PartialLatticeType a) → PartialLatticeType.EltType plt → PartialLatticeType.EltType plt → Maybe (PartialLatticeType.EltType plt)

lvCombine : ∀ {a} (f : CombineForPLT a) (l : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue l) →  Maybe (ListValue l)
lvCombine _ [] _ _ = nothing
lvCombine f (plt ∷ plts) (inj₁ v₁) (inj₁ v₂) = Maybe.map inj₁ (f plt v₁ v₂)
lvCombine f (_ ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = Maybe.map inj₂ (lvCombine f plts lv₁ lv₂)
lvCombine _ (_ ∷ plts) (inj₁ _) (inj₂ _) = nothing
lvCombine _ (_ ∷ plts) (inj₂ _) (inj₁ _) = nothing

lvJoin : ∀ {a} (l : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue l) →  Maybe (ListValue l)
lvJoin = lvCombine PartialLatticeType._⊔?_

lvMeet : ∀ {a} (l : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue l) →  Maybe (ListValue l)
lvMeet = lvCombine PartialLatticeType._⊓?_

pathJoin' : ∀ {a} (Ls : Layers a) (p₁ p₂ : Path' Ls) →  Maybe (Path' Ls)
pathJoin' (single l) lv₁ lv₂ = lvJoin (toList l) lv₁ lv₂
pathJoin' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvJoin (toList l) lv₁ lv₂)
pathJoin' (add-via-least l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₁ lv₁)
pathJoin' (add-via-least l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂)
pathJoin' (add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls) (inj₂ p₁) (inj₂ p₂)
    with pathJoin' ls p₁ p₂
...   | just p = just (inj₂ p)
...   | nothing = just (inj₁ (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasLeast)))
pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvJoin (toList l) lv₁ lv₂)
pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₁ lv₁)
pathJoin' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂)
pathJoin' (add-via-greatest l ls {{greatest}}) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathJoin' ls p₁ p₂) -- not our job to provide the least element here. If there was a "greatest" there, recursion would've found it (?)

pathMeet' : ∀ {a} (Ls : Layers a) (p₁ p₂ : Path' Ls) →  Maybe (Path' Ls)
pathMeet' (single l) lv₁ lv₂ = lvMeet (toList l) lv₁ lv₂
pathMeet' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvMeet (toList l) lv₁ lv₂)
pathMeet' (add-via-least l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₂ p₂)
pathMeet' (add-via-least l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₂ p₁)
pathMeet' (add-via-least l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ p₂)
pathMeet' (add-via-greatest l ls {{greatest}}) (inj₁ lv₁) (inj₁ lv₂)
    with lvMeet (toList l) lv₁ lv₂
...   | just lv = just (inj₁ lv)
...   | nothing
        with head ls | greatest | valueAtHead ls
...       | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
          = just (inj₂ (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest))))
pathMeet' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₂ p₂)
pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₂ p₁)
pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ p₂)

eqL : ∀ {a} (L : List (PartialLatticeType a)) →  ListValue L → ListValue L → Set a
eqL [] ()
eqL (plt ∷ plts) (inj₁ v₁ ) (inj₁ v₂) = PartialLattice._≈_ (PartialLatticeType.partialLattice plt) v₁ v₂
eqL (plt ∷ plts) (inj₂ v₁ ) (inj₂ v₂) = eqL plts v₁ v₂
eqL (plt ∷ plts) (inj₁ _) (inj₂ _) = Empty _
eqL (plt ∷ plts) (inj₂ _) (inj₁ _) = Empty _

eqL-refl : ∀ {a} (L : List (PartialLatticeType a)) (lv : ListValue L) →  eqL L lv lv
eqL-refl [] ()
eqL-refl (plt ∷ plts) (inj₁ v) = IsEquivalence.≈-refl (PartialLatticeType.≈-equiv plt)
eqL-refl (plt ∷ plts) (inj₂ v) = eqL-refl plts v

eqLv : ∀ {a} (L : Layer a) →  LayerValue L → LayerValue L → Set a
eqLv L = eqL (toList L)

eqLv-refl : ∀ {a} (L : Layer a) →  (lv : LayerValue L) → eqLv L lv lv
eqLv-refl L = eqL-refl (toList L)

eqPath' : ∀ {a} (Ls : Layers a) → Path' Ls → Path' Ls → Set a
eqPath' (single l) lv₁ lv₂ = eqLv l lv₁ lv₂
eqPath' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = eqLv l lv₁ lv₂
eqPath' (add-via-least l ls) (inj₂ p₁) (inj₂ p₂) = eqPath' ls p₁ p₂
eqPath' (add-via-least l ls) (inj₁ lv₁) (inj₂ p₂) = Empty _
eqPath' (add-via-least l ls) (inj₂ p₁) (inj₁ lv₂) = Empty _
eqPath' (add-via-greatest l ls) (inj₁ lv₁) (inj₁ lv₂) = eqLv l lv₁ lv₂
eqPath' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = eqPath' ls p₁ p₂
eqPath' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = Empty _
eqPath' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = Empty _

eqPath'-refl : ∀ {a} (Ls : Layers a) →  (p : Path' Ls) →  eqPath' Ls p p
eqPath'-refl (single l) lv = eqLv-refl l lv
eqPath'-refl (add-via-least l ls) (inj₁ lv) = eqLv-refl l lv
eqPath'-refl (add-via-least l ls) (inj₂ p) = eqPath'-refl ls p
eqPath'-refl (add-via-greatest l ls) (inj₁ lv) = eqLv-refl l lv
eqPath'-refl (add-via-greatest l ls) (inj₂ p) = eqPath'-refl ls p

-- Now that we can compare paths for "equality", we can state and
-- prove theorems such as commutativity and idempotence.

data Expr {a} (A : Set a) : Set a where
    `_ : A →  Expr A
    _∨_ : Expr A → Expr A → Expr A

map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → Expr A → Expr B
map f (` x) = ` (f x)
map f (e₁ ∨ e₂) = map f e₁ ∨ map f e₂

eval : ∀ {a} {A : Set a} (_⊔?_ : A → A → Maybe A) (e : Expr A) → Maybe A
eval _⊔?_ (` x) = just x
eval _⊔?_ (e₁ ∨ e₂) = (eval _⊔?_ e₁) >>= (λ v₁ →  (eval _⊔?_ e₂) >>= (v₁ ⊔?_))

-- the two lvCombine homomorphism properties essentially say that, when all layer values
-- are from the same type, the lvCombine preserves the structure of operations
-- on these layer values.

lvCombine-homo₁ : ∀ {a} plt plts (f : CombineForPLT a) (e : Expr (PartialLatticeType.EltType plt)) → eval (lvCombine f (plt ∷ plts)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (f plt) e)
lvCombine-homo₁ plt plts f (` _) = refl
lvCombine-homo₁ plt plts f (e₁ ∨ e₂)
    rewrite lvCombine-homo₁ plt plts f e₁ rewrite lvCombine-homo₁ plt plts f e₂
    with eval (f plt) e₁ | eval (f plt) e₂
...   | just x₁ | just x₂ = refl
...   | nothing | nothing = refl
...   | just x₁ | nothing = refl
...   | nothing | just x₂ = refl

lvCombine-homo₂ : ∀ {a} plt plts (f : CombineForPLT a) (e : Expr (ListValue plts)) → eval (lvCombine f (plt ∷ plts)) (map inj₂ e) ≡ Maybe.map inj₂ (eval (lvCombine f plts) e)
lvCombine-homo₂ plt plts f (` _) = refl
lvCombine-homo₂ plt plts f (e₁ ∨ e₂)
    rewrite lvCombine-homo₂ plt plts f e₁ rewrite lvCombine-homo₂ plt plts f e₂
    with eval (lvCombine f plts) e₁ | eval (lvCombine f plts) e₂
...   | just x₁ | just x₂ = refl
...   | nothing | nothing = refl
...   | just x₁ | nothing = refl
...   | nothing | just x₂ = refl

lvCombine-assoc : ∀ {a} (f : CombineForPLT a) →
                  (∀ plt →  PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) →
                  ∀ (L : List (PartialLatticeType a)) →
                  PartialAssoc (eqL L) (lvCombine f L)
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ v₁) (inj₁ v₂) (inj₁ v₃)
    rewrite lvCombine-homo₁ plt plts f (((` v₁) ∨ (` v₂)) ∨ (` v₃))
    rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ ((` v₂) ∨ (` v₃)))
    = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-assoc plt v₁ v₂ v₃)
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ _) (inj₁ v₂) (inj₁ v₃)
    with f plt v₂ v₃
...   | just _ = ≈-nothing
...   | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ _) (inj₂ _) (inj₁ _) = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₁ _)
    with lvCombine f plts lv₁ lv₂
...   | just _ = ≈-nothing
...   | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ v₁) (inj₁ v₂) (inj₂ _)
    with f plt v₁ v₂
...   | just _ = ≈-nothing
...   | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ _) (inj₁ _) (inj₂ _) = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ _) (inj₂ lv₂) (inj₂ lv₃)
    with lvCombine f plts lv₂ lv₃
...   | just _ = ≈-nothing
...   | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₂ lv₃)
    rewrite lvCombine-homo₂ plt plts f (((` lv₁) ∨ (` lv₂)) ∨ (` lv₃))
    rewrite lvCombine-homo₂ plt plts f ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃)))
    = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-assoc f f-assoc plts lv₁ lv₂ lv₃)

lvCombine-comm : ∀ {a} (f : CombineForPLT a) →
                 (∀ plt →  PartialComm (PartialLatticeType._≈_ plt) (f plt)) →
                 ∀ (L : List (PartialLatticeType a)) →
                 PartialComm (eqL L) (lvCombine f L)
lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂)
    rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ (` v₂)) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-comm plt v₁ v₂)
lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-comm f f-comm plts lv₁ lv₂)
lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing
lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing

lvCombine-idemp : ∀ {a} (f : CombineForPLT a) →
                  (∀ plt →  PartialIdemp (PartialLatticeType._≈_ plt) (f plt)) →
                  ∀ (L : List (PartialLatticeType a)) →
                  PartialIdemp (eqL L) (lvCombine f L)
lvCombine-idemp f f-idemp (plt ∷ plts) (inj₁ v) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-idemp plt v)
lvCombine-idemp f f-idemp (plt ∷ plts) (inj₂ lv) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-idemp f f-idemp plts lv)

lvJoin-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvJoin L)
lvJoin-assoc = lvCombine-assoc PartialLatticeType._⊔?_ PartialLatticeType.⊔-assoc

lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L)
lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm

lvJoin-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvJoin L)
lvJoin-idemp = lvCombine-idemp PartialLatticeType._⊔?_ PartialLatticeType.⊔-idemp

lvMeet-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvMeet L)
lvMeet-assoc = lvCombine-assoc PartialLatticeType._⊓?_ PartialLatticeType.⊓-assoc

lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvMeet L)
lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm

lvMeet-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L)
lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp

pathJoin'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathJoin' Ls)
pathJoin'-comm {Ls = single l} lv₁ lv₂ = lvJoin-comm (toList l) lv₁ lv₂
pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂)
pathJoin'-comm {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
    with pathJoin' ls p₁ p₂ | pathJoin' ls p₂ p₁ | pathJoin'-comm {Ls = ls} p₁ p₂
...   | just p | just p' | ≈-just p≈p' = ≈-just p≈p'
...   | nothing | nothing | ≈-nothing = ≈-just (eqLv-refl l (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasLeast)))
pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqLv-refl l lv₁)
pathJoin'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqLv-refl l lv₂)
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂)
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathJoin'-comm {Ls = ls} p₁ p₂)
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqLv-refl l lv₁)
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqLv-refl l lv₂)

pathMeet'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathMeet' Ls)
pathMeet'-comm {Ls = single l} lv₁ lv₂ = lvMeet-comm (toList l) lv₁ lv₂
pathMeet'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-comm (toList l) lv₁ lv₂)
pathMeet'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-comm {Ls = ls} p₁ p₂)
pathMeet'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqPath'-refl ls p₂)
pathMeet'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqPath'-refl ls p₁)
pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
    with lvMeet (toList l) lv₁ lv₂ | lvMeet (toList l) lv₂ lv₁ | lvMeet-comm (toList l) lv₁ lv₂
...   | just lv | just lv' | ≈-just lv≈lv' = ≈-just lv≈lv'
...   | nothing | nothing | ≈-nothing
        with ls | greatest | valueAtHead ls
-- begin dumb: don't know why, but abstracting on `head ls` leads to an ill-formed case
...       | single l' | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
          = ≈-just (eqLv-refl l' (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest))))
...       | add-via-least l' {{least = least}} ls' | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
          = ≈-just (eqPath'-refl (add-via-least l' {{least}} ls') (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest))))
...       | add-via-greatest l' ls' {{greatest = greatest'}} | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
          = ≈-just (eqPath'-refl (add-via-greatest l' ls' {{greatest'}}) (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest))))
-- end dumb
pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-comm {Ls = ls} p₁ p₂)
pathMeet'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqPath'-refl ls p₂)
pathMeet'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqPath'-refl ls p₁)

record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
    field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)

_⊔̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls)
_⊔̇_ {a} {ls} p₁ p₂ = Maybe.map MkPath (pathJoin' ls (Path.path p₁) (Path.path p₂))

_⊓̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls)
_⊓̇_ {a} {ls} p₁ p₂ = Maybe.map MkPath (pathMeet' ls (Path.path p₁) (Path.path p₂))

-- 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)
--     there : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)} →
--              ListValue pltl → ListValue (plt ∷ pltl)