DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add instances of semilattice proofs

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-25 17:18:19 +02:00
parent 42bb8f8792
commit 2808759338
1 changed files with 20 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
Lattice/Builder.agda
View File

@ -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)