From c6dddb177ef4dfc00f1fc431e7129dce557ae9ce Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 13 Jul 2023 23:22:29 -0700
Subject: [PATCH] Get started on a lattice instance for naturals.

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

diff --git a/Lattice.agda b/Lattice.agda
index 6b3ef05..c514f4d 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -153,3 +153,14 @@ private module NatInstances where
             ; ⊔-least = min-greatest
             }
         }
+
+    NatLattice : Lattice ℕ
+    NatLattice = record
+        { _≼_ = _≤_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = record
+            { joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice
+            ; meetSemilattice = Semilattice.isSemilattice NatMinSemilattice
+            }
+        }