From 42bb8f879245d553a4e478be9700761c321c958e Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 25 Jul 2025 17:17:59 +0200
Subject: [PATCH] Extend laws on Path' to Path versions

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Builder.agda | 52 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index b9ed96f..44ead6d 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -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)
 
 record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
+    constructor mk-≈
     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} 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} 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
 --     here : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)}
 --              (v : PartialLatticeType.EltType plt) → ListValue (plt ∷ pltl)