Add bundles to 'AboveBelow'

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

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