From c932210d3726089cc40fcb1d37c36098b8722f21 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 3 Mar 2024 17:04:18 -0800
Subject: [PATCH] Re-expert monotonicity from Lattice

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Lattice.agda b/Lattice.agda
index c9a9154..2feb2f5 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -120,6 +120,8 @@ record IsLattice {a} (A : Set a)
         ( ⊔-assoc to ⊓-assoc
         ; ⊔-comm to ⊓-comm
         ; ⊔-idemp to ⊓-idemp
+        ; ⊔-Monotonicˡ to ⊓-Monotonicˡ
+        ; ⊔-Monotonicʳ to ⊓-Monotonicʳ
         ; ≈-⊔-cong to ≈-⊓-cong
         ; _≼_ to _≽_
         ; _≺_ to _≻_