diff --git a/Lattice.agda b/Lattice.agda
index d50664b..22769dc 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -29,6 +29,7 @@ record IsSemilattice {a} (A : Set a)
 
     field
         ≈-equiv : IsEquivalence A _≈_
+        ≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔ a₃) ≈ (a₂ ⊔ a₄)
 
         ⊔-assoc : (x y z : A) → ((x ⊔ y) ⊔ z) ≈ (x ⊔ (y ⊔ z))
         ⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x)
@@ -56,6 +57,7 @@ record IsLattice {a} (A : Set a)
         ( ⊔-assoc to ⊓-assoc
         ; ⊔-comm to ⊓-comm
         ; ⊔-idemp to ⊓-idemp
+        ; ≈-⊔-cong to ≈-⊓-cong
         ; _≼_ to _≽_
         ; _≺_ to _≻_
         ; ≼-refl to ≽-refl
@@ -120,6 +122,13 @@ module IsSemilatticeInstances where
         open NatProps
         open Eq
 
+        private
+            ≡-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊔ a₃) ≡ (a₂ ⊔ a₄)
+            ≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
+
+            ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
+            ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
+
         NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
         NatIsMaxSemilattice = record
             { ≈-equiv = record
@@ -127,6 +136,7 @@ module IsSemilatticeInstances where
                 ; ≈-sym = sym
                 ; ≈-trans = trans
                 }
+            ; ≈-⊔-cong = ≡-⊔-cong
             ; ⊔-assoc = ⊔-assoc
             ; ⊔-comm = ⊔-comm
             ; ⊔-idemp = ⊔-idem
@@ -139,6 +149,7 @@ module IsSemilatticeInstances where
                 ; ≈-sym = sym
                 ; ≈-trans = trans
                 }
+            ; ≈-⊔-cong = ≡-⊓-cong
             ; ⊔-assoc = ⊓-assoc
             ; ⊔-comm = ⊓-comm
             ; ⊔-idemp = ⊓-idem
@@ -163,6 +174,10 @@ module IsSemilatticeInstances where
         ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
         ProdIsSemilattice = record
             { ≈-equiv = ProdEquiv.ProdEquivalence
+            ; ≈-⊔-cong = λ (a₁≈a₂ , b₁≈b₂) (a₃≈a₄ , b₃≈b₄) →
+                ( IsSemilattice.≈-⊔-cong sA a₁≈a₂ a₃≈a₄
+                , IsSemilattice.≈-⊔-cong sB b₁≈b₂ b₃≈b₄
+                )
             ; ⊔-assoc = λ (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) →
                 ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
                 , IsSemilattice.⊔-assoc sB b₁ b₂ b₃
@@ -185,7 +200,7 @@ module IsSemilatticeInstances where
 
         open import Map A B ≡-dec-A
         open IsSemilattice sB renaming
-            ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
+            ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-⊔-cong to ≈₂-⊔₂-cong
             ; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
             )
 
@@ -204,6 +219,7 @@ module IsSemilatticeInstances where
         MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
         MapIsUnionSemilattice = record
             { ≈-equiv = MapEquiv.LiftEquivalence
+            ; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} → union-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
             ; ⊔-assoc = union-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
             ; ⊔-comm = union-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
             ; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
@@ -212,6 +228,7 @@ module IsSemilatticeInstances where
         MapIsIntersectSemilattice : IsSemilattice Map _≈_ _⊓_
         MapIsIntersectSemilattice = record
             { ≈-equiv = MapEquiv.LiftEquivalence
+            ; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} → intersect-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
             ; ⊔-assoc = intersect-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
             ; ⊔-comm = intersect-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
             ; ⊔-idemp = intersect-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp