From 33b7bc37f06cbaacf2e544fdbeeb6e54072bfe2a Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 14:17:49 -0800
Subject: [PATCH] Add a 'FiniteHeightLattice' bundle

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

diff --git a/Lattice.agda b/Lattice.agda
index c06b2bc..353e8d5 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -145,3 +145,14 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
         isLattice : IsLattice A _≈_ _⊔_ _⊓_
 
     open IsLattice isLattice public
+
+record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
+    field
+        height : ℕ
+        _≈_ : A → A → Set a
+        _⊔_ : A → A → A
+        _⊓_ : A → A → A
+
+        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊔_
+
+    open IsFiniteHeightLattice isFiniteHeightLattice public