From 14f1494fc30d1c157c62f34b14d5f61a342f9f81 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 22 Jul 2025 18:01:48 +0200 Subject: [PATCH] Provide a definition of partial congruence Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 33dd459..8102dfa 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -3,6 +3,7 @@ module Lattice.Builder where open import Lattice open import Equivalence open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe) +open import Data.Maybe.Properties using (just-injective) open import Data.Unit using (⊤; tt) open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_) open import Data.List using (List; _∷_; []) @@ -42,6 +43,9 @@ instance } } +PartialCong : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a +PartialCong {a} {A} _≈_ _⊗_ = ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → lift-≈ _≈_ (a₁ ⊗ a₃) (a₂ ⊗ 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 ⊗_)) @@ -69,7 +73,7 @@ record IsPartialSemilattice {a} {A : Set a} field ≈-equiv : IsEquivalence A _≈_ - ≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔? a₃) ≈? (a₂ ⊔? a₄) + ≈-⊔-cong : PartialCong _≈_ _⊔?_ ⊔-assoc : PartialAssoc _≈_ _⊔?_ ⊔-comm : PartialComm _≈_ _⊔?_