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

Prove the other absorption law

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-25 19:26:03 +02:00
parent 706b593d1d
commit fbb98de40f
1 changed files with 34 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
Lattice/Builder.agda
View File

@ -1025,6 +1025,40 @@ absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj
(λ _ _ → refl) (λ _ _ → refl)
(absorb-pathJoin'-pathMeet' {Ls = ls}) p₁ p₂
absorb-pathMeet'-pathJoin' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathMeet' Ls) (pathJoin' Ls)
absorb-pathMeet'-pathJoin' {Ls = single l} lv₁ lv₂ = absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
= PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvMeet (toList l)) (lvJoin (toList l))
(pathMeet' Ls) (pathJoin' Ls)
(λ _ _ → refl) (λ _ _ → refl)
(absorb-lvMeet-lvJoin (toList l)) lv₁ lv₂
absorb-pathMeet'-pathJoin' {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂)
= ≈-just (eqPath'-refl ls p₁)
absorb-pathMeet'-pathJoin' {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂)
= pathMeet'-idemp {Ls = add-via-least l {{least}} ls} (inj₁ lv₁)
absorb-pathMeet'-pathJoin' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
with pathJoin' ls p₁ p₂ | absorb-pathMeet'-pathJoin' {Ls = ls} p₁ p₂
... | nothing | _ = ≈-just (eqPath'-refl ls p₁)
... | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
with pathMeet' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
... | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
with lvJoin (toList l) lv₁ lv₂ | absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
... | nothing | _ = mkTrivial
... | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
with lvMeet (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
... | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂)
= ≈-just (eqPath'-refl ls p₁)
absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂)
= pathMeet'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁)
absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
= PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathMeet' ls) (pathJoin' ls)
(pathMeet' Ls) (pathJoin' Ls)
(λ _ _ → refl) (λ _ _ → refl)
(absorb-pathMeet'-pathJoin' {Ls = ls}) p₁ p₂
record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
constructor mk-≈
field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)