diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index f9f2374..4ba0465 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -129,10 +129,6 @@ record IsPartialSemilattice {a} {A : Set 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₂
-Maybe-≈ {a} _≈_ nothing a₂ = Trivial a
-
 record IsPartialLattice {a} {A : Set a}
     (_≈_ : A → A → Set a)
     (_⊔?_ : A → A → Maybe A)
@@ -142,8 +138,8 @@ record IsPartialLattice {a} {A : Set a}
         {{partialJoinSemilattice}} : IsPartialSemilattice _≈_ _⊔?_
         {{partialMeetSemilattice}} : IsPartialSemilattice _≈_ _⊓?_
 
-        absorb-⊔-⊓ : (x y : A) →  Maybe-≈ _≈_ ((x ⊓? y) >>= (x ⊔?_)) x
-        absorb-⊓-⊔ : (x y : A) →  Maybe-≈ _≈_ ((x ⊔? y) >>= (x ⊓?_)) x
+        absorb-⊔-⊓ : (x y : A) →  maybe (λ x⊓y → lift-≈ _≈_ (x ⊔? x⊓y) (just x)) (Trivial _) (x ⊓? y)
+        absorb-⊓-⊔ : (x y : A) →  maybe (λ x⊔y → lift-≈ _≈_ (x ⊓? x⊔y) (just x)) (Trivial _) (x ⊔? y)
 
     open IsPartialSemilattice partialJoinSemilattice public
     open IsPartialSemilattice partialMeetSemilattice using ()