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 + } + }