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

Show that lifted equality preserves equivalences

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-05 14:52:40 -07:00
parent da6e82d04b
commit d251915772
1 changed files with 16 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
Lattice/Builder.agda
View File

@ -29,6 +29,22 @@ lift-≈-map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ (just a₁) (just a₂) (≈-just a₁≈a₂) = ≈-just (≈ᵃ→≈ᵇ a₁ a₂ a₁≈a₂) lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ (just a₁) (just a₂) (≈-just a₁≈a₂) = ≈-just (≈ᵃ→≈ᵇ a₁ a₂ a₁≈a₂)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ nothing nothing ≈-nothing = ≈-nothing lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ nothing nothing ≈-nothing = ≈-nothing
instance
lift-≈-Equivalence : ∀ {a} {A : Set a} {_≈_ : A → A → Set a} {{isEquivalence : IsEquivalence A _≈_}} → IsEquivalence (Maybe A) (lift-≈ _≈_)
lift-≈-Equivalence {{isEquivalence}} = record
{ ≈-trans =
(λ { (≈-just a₁≈a₂) (≈-just a₂≈a₃) → ≈-just (IsEquivalence.≈-trans isEquivalence a₁≈a₂ a₂≈a₃)
; ≈-nothing ≈-nothing → ≈-nothing
})
; ≈-sym =
(λ { (≈-just a₁≈a₂) → ≈-just (IsEquivalence.≈-sym isEquivalence a₁≈a₂)
; ≈-nothing → ≈-nothing
})
; ≈-refl = λ { {just a} → ≈-just (IsEquivalence.≈-refl isEquivalence)
; {nothing} → ≈-nothing
}
}
PartialAssoc : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a PartialAssoc : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialAssoc {a} {A} _≈_ _⊗_ = ∀ (x y z : A) → lift-≈ _≈_ ((x ⊗ y) >>= (_⊗ z)) ((y ⊗ z) >>= (x ⊗_)) PartialAssoc {a} {A} _≈_ _⊗_ = ∀ (x y z : A) → lift-≈ _≈_ ((x ⊗ y) >>= (_⊗ z)) ((y ⊗ z) >>= (x ⊗_))