From 27f40bd42eba3967155917e44f29f3cd0689c57f Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 21:00:28 -0800
Subject: [PATCH] Add bundles to 'AboveBelow'

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

diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda
index 30e1ea3..6056e30 100644
--- a/Lattice/AboveBelow.agda
+++ b/Lattice/AboveBelow.agda
@@ -279,6 +279,14 @@ module Plain where
         ; absorb-⊓-⊔ = absorb-⊓-⊔
         }
 
+    lattice : Lattice AboveBelow
+    lattice = record
+        { _≈_ = _≈_
+        ; _⊔_ = _⊔_
+        ; _⊓_ = _⊓_
+        ; isLattice = isLattice
+        }
+
     open IsLattice isLattice using (_≼_; _≺_)
 
     ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ]
@@ -329,3 +337,12 @@ module Plain where
             { isLattice = isLattice
             ; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
             }
+
+        finiteHeightLattice : FiniteHeightLattice AboveBelow
+        finiteHeightLattice = record
+            { height = 2
+            ; _≈_ = _≈_
+            ; _⊔_ = _⊔_
+            ; _⊓_ = _⊓_
+            ; isFiniteHeightLattice = isFiniteHeightLattice
+            }