From b1c6b4c99a0c14353cc56054b5dee5d5913da05a Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 21:20:05 -0800
Subject: [PATCH] Expose bundles from Unit

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

diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda
index d736dbe..c16bcc5 100644
--- a/Lattice/Unit.agda
+++ b/Lattice/Unit.agda
@@ -89,6 +89,14 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
+lattice : Lattice ⊤
+lattice = record
+    { _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isLattice = isLattice
+    }
+
 open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
 
 private
@@ -104,3 +112,12 @@ isFiniteHeightLattice = record
     { isLattice = isLattice
     ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
     }
+
+finiteHeightLattice : FiniteHeightLattice ⊤
+finiteHeightLattice = record
+    { height = 0
+    ; _≈_ = _≈_
+    ; _⊔_ = _⊔_
+    ; _⊓_ = _⊓_
+    ; isFiniteHeightLattice = isFiniteHeightLattice
+    }