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

Extend laws on Path' to Path versions

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

52
Lattice/Builder.agda
View File

@ -950,14 +950,66 @@ pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₁ lv)
pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p) pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
constructor mk-≈
field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂) field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)
instance
≈-Equivalence : ∀ {a} {Ls : Layers a} → IsEquivalence (Path Ls) (_≈_ {Ls = Ls})
≈-Equivalence {Ls = Ls} =
record
{ ≈-refl = λ {(MkPath p)} → mk-≈ (eqPath'-refl Ls p)
; ≈-sym = λ (mk-≈ p≈p') → mk-≈ (eqPath'-sym Ls p≈p')
; ≈-trans = λ (mk-≈ p₁≈p₂) (mk-≈ p₂≈p₃) → mk-≈ (eqPath'-trans Ls p₁≈p₂ p₂≈p₃)
}
_⊔̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls) _⊔̇_ : ∀ {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} p₁ p₂ = Maybe.map MkPath (pathJoin' ls (Path.path p₁) (Path.path p₂))
_⊔̇_-subHomo : ∀ {a} (Ls : Layers a) (e : Expr (Path' Ls)) → eval (_⊔̇_ {Ls = Ls}) (map MkPath e) ≡ Maybe.map MkPath (eval (pathJoin' Ls) e)
_⊔̇_-subHomo Ls e = eval-subHomo MkPath (pathJoin' Ls) _⊔̇_ e (λ a₁ a₂ → refl)
_⊔̇_-comm : ∀ {a} {Ls : Layers a} → PartialComm (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
_⊔̇_-comm {Ls = Ls} (MkPath p₁) (MkPath p₂)
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-comm {Ls = Ls} p₁ p₂)
_⊔̇_-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
_⊔̇_-assoc {Ls = Ls} (MkPath p₁) (MkPath p₂) (MkPath p₃)
rewrite _⊔̇_-subHomo Ls (((` p₁) ∨ (` p₂)) ∨ (` p₃))
rewrite _⊔̇_-subHomo Ls ((` p₁) ∨ ((` p₂) ∨ (` p₃)))
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-assoc {Ls = Ls} p₁ p₂ p₃)
_⊔̇_-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
_⊔̇_-idemp {Ls = Ls} (MkPath p)
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-idemp {Ls = Ls} p)
≈-⊔̇-cong : ∀ {a} {Ls : Layers a} → PartialCong (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
≈-⊔̇-cong {Ls = Ls} (mk-≈ p₁≈p₂) (mk-≈ p₃≈p₄) =
lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (eqPath'-pathJoin'-cong {Ls = Ls} p₁≈p₂ p₃≈p₄)
_⊓̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls) _⊓̇_ : ∀ {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₂)) _⊓̇_ {a} {ls} p₁ p₂ = Maybe.map MkPath (pathMeet' ls (Path.path p₁) (Path.path p₂))
_⊓̇_-subHomo : ∀ {a} (Ls : Layers a) (e : Expr (Path' Ls)) → eval (_⊓̇_ {Ls = Ls}) (map MkPath e) ≡ Maybe.map MkPath (eval (pathMeet' Ls) e)
_⊓̇_-subHomo Ls e = eval-subHomo MkPath (pathMeet' Ls) _⊓̇_ e (λ a₁ a₂ → refl)
_⊓̇_-comm : ∀ {a} {Ls : Layers a} → PartialComm (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
_⊓̇_-comm {Ls = Ls} (MkPath p₁) (MkPath p₂)
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-comm {Ls = Ls} p₁ p₂)
_⊓̇_-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
_⊓̇_-assoc {Ls = Ls} (MkPath p₁) (MkPath p₂) (MkPath p₃)
rewrite _⊓̇_-subHomo Ls (((` p₁) ∨ (` p₂)) ∨ (` p₃))
rewrite _⊓̇_-subHomo Ls ((` p₁) ∨ ((` p₂) ∨ (` p₃)))
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-assoc {Ls = Ls} p₁ p₂ p₃)
_⊓̇_-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
_⊓̇_-idemp {Ls = Ls} (MkPath p)
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-idemp {Ls = Ls} p)
≈-⊓̇-cong : ∀ {a} {Ls : Layers a} → PartialCong (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
≈-⊓̇-cong {Ls = Ls} (mk-≈ p₁≈p₂) (mk-≈ p₃≈p₄) =
lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (eqPath'-pathMeet'-cong {Ls = Ls} p₁≈p₂ p₃≈p₄)
-- data ListValue {a : Level} : List (PartialLatticeType a) → Set (lsuc a) where -- data ListValue {a : Level} : List (PartialLatticeType a) → Set (lsuc a) where
-- here : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)} -- here : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)}
-- (v : PartialLatticeType.EltType plt) → ListValue (plt ∷ pltl) -- (v : PartialLatticeType.EltType plt) → ListValue (plt ∷ pltl)