diff --git a/Lattice/Nat.agda b/Lattice/Nat.agda
index c3f760a..64f1247 100644
--- a/Lattice/Nat.agda
+++ b/Lattice/Nat.agda
@@ -18,8 +18,8 @@ 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
 
-NatIsMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
-NatIsMaxSemilattice = record
+isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
+isMaxSemilattice = record
     { ≈-equiv = record
         { ≈-refl = refl
         ; ≈-sym = sym
@@ -31,8 +31,8 @@ NatIsMaxSemilattice = record
     ; ⊔-idemp = ⊔-idem
     }
 
-NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
-NatIsMinSemilattice = record
+isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
+isMinSemilattice = record
     { ≈-equiv = record
         { ≈-refl = refl
         ; ≈-sym = sym
@@ -74,10 +74,18 @@ private
             helper : x ⊔ (x ⊓ y) ≤ x ⊔ x  → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
             helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
 
-NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
-NatIsLattice = record
-    { joinSemilattice = NatIsMaxSemilattice
-    ; meetSemilattice = NatIsMinSemilattice
+isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
+isLattice = record
+    { joinSemilattice = isMaxSemilattice
+    ; meetSemilattice = isMinSemilattice
     ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
     ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
     }
+
+lattice : Lattice ℕ
+lattice = record
+    { _≈_ = _≡_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }