From d2faada90adab6102d14842891735a82925ba5f4 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 11 Jul 2025 15:43:27 +0200 Subject: [PATCH] Add a left and right version of identity Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 7aaeec3..f9f2374 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -124,7 +124,10 @@ record IsPartialSemilattice {a} {A : Set a} field x : A not-partial : ∀ (a₁ a₂ : A) → Σ A (λ a₃ → (a₁ ⊔? a₂) ≡ just a₃) - x-identity : (a : A) → (x ⊔? a) ≈? just a + x-identityˡ : (a : A) → (x ⊔? a) ≈? just a + + x-identityʳ : (a : A) → (a ⊔? x) ≈? just a + x-identityʳ a = ≈?-trans (⊔-comm a x) (x-identityˡ a) Maybe-≈ : ∀ {a} {A : Set a} → (_≈_ : A → A → Set a) → Maybe A → A → Set a Maybe-≈ _≈_ (just a₁) a₂ = a₁ ≈ a₂