Get started on a lattice instance for naturals.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2023-07-13 23:22:29 -07:00 · 2023-07-13 23:22:29 -07:00 · c6dddb177e
commit c6dddb177e
parent 422ea93edb
1 changed files with 11 additions and 0 deletions
--- 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
+            }
+        }