diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda new file mode 100644 index 0000000..b59e414 --- /dev/null +++ b/Lattice/Builder.agda @@ -0,0 +1,329 @@ +module Lattice.Builder where + +open import Lattice +open import Equivalence +open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_) +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 Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) +open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) + +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-≈-to-≈' : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_≈'_ : A → A → Set a) → +-- (∀ x y → (x ≈ y) ≡ (x ≈' y)) → +-- ∀ m₁ m₂ → lift-≈ _≈_ m₁ m₂ → lift-≈ _≈'_ m₁ m₂ +-- lift-≈-to-≈' _≈_ _≈'_ ≈≡≈' (just x₁) (just x₂) (≈-just x₁≈x₂) +-- rewrite ≈≡≈' x₁ x₂ = ≈-just x₁≈x₂ +-- lift-≈-to-≈' _≈_ _≈'_ ≈≡≈' m₁ m₂ ≈-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 + +record IsPartialSemilattice {a} {A : Set a} + (_≈_ : A → A → Set a) + (_⊔?_ : A → A → Maybe A) : Set a where + + _≈?_ : Maybe A → Maybe A → Set a + _≈?_ = lift-≈ _≈_ + + field + ≈-equiv : IsEquivalence A _≈_ + ≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔? a₃) ≈? (a₂ ⊔? a₄) + + ⊔-assoc : (x y z : A) → ((x ⊔? y) >>= (_⊔? z)) ≈? ((y ⊔? z) >>= (x ⊔?_)) + ⊔-comm : (x y : A) → (x ⊔? y) ≈? (y ⊔? x) + ⊔-idemp : (x : A) → (x ⊔? x) ≈? just x + + 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 + +data Trivial a : Set a where + instance + mkTrivial : Trivial a + +data Empty a : Set a where + +Maybe-≈ : ∀ {a} {A : Set a} → (_≈_ : A → A → Set a) → Maybe A → A → Set a +Maybe-≈ _≈_ (just a₁) a₂ = a₁ ≈ a₂ +Maybe-≈ {a} _≈_ nothing a₂ = Trivial 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) >>= (x ⊔?_)) x + absorb-⊓-⊔ : (x y : A) → Maybe-≈ _≈_ ((x ⊔? y) >>= (x ⊓?_)) x + + 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₂) + with f plt v₁ v₂ +... | just v = just (inj₁ v) +... | nothing = nothing +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. + +lvCombine-comm : ∀ {a} (f : CombineForPLT a) → + (∀ plt v₁ v₂ → PartialLatticeType._≈?_ plt (f plt v₁ v₂) (f plt v₂ v₁)) → + ∀ (L : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue L) → + lift-≈ (eqL L) (lvCombine f L lv₁ lv₂) (lvCombine f L lv₂ lv₁) +lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂) + with f plt v₁ v₂ + | f plt v₂ v₁ + | f-comm plt v₁ v₂ +... | _ | _ | ≈-just v₁v₂≈v₂v₁ = ≈-just v₁v₂≈v₂v₁ +... | _ | _ | ≈-nothing = ≈-nothing +lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) + with lvCombine f plts lv₁ lv₂ | lvCombine f plts lv₂ lv₁ | lvCombine-comm f f-comm plts lv₁ lv₂ +... | _ | _ | ≈-just lv₁lv₂≈lv₂lv₁ = ≈-just lv₁lv₂≈lv₂lv₁ +... | _ | _ | ≈-nothing = ≈-nothing +lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing +lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing + +lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue L) → lift-≈ (eqL L) (lvJoin L lv₁ lv₂) (lvJoin L lv₂ lv₁) +lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm + +lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue L) → lift-≈ (eqL L) (lvMeet L lv₁ lv₂) (lvMeet L lv₂ lv₁) +lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm + +pathJoin'-comm : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path' Ls) → lift-≈ (eqPath' Ls) (pathJoin' Ls p₁ p₂) (pathJoin' Ls p₂ p₁) +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} (p₁ p₂ : Path' Ls) → lift-≈ (eqPath' Ls) (pathMeet' Ls p₁ p₂) (pathMeet' Ls p₂ p₁) +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)