diff --git a/Lattice.agda b/Lattice.agda
index 2feb2f5..dbe0ade 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -103,6 +103,17 @@ record IsSemilattice {a} (A : Set a)
         , λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄)))
         )
 
+module _ {a b} {A : Set a} {B : Set b}
+         {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}
+         {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
+         (lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where
+
+    open IsSemilattice lA using () renaming (_≼_ to _≼₁_)
+    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp)
+
+    const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
+    const-Mono x _ = ⊔₂-idemp x
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)