Add instances for decidability and finite height lattices

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

Lattice.agda

@@ -3,12 +3,12 @@ module Lattice where
 import Data.Nat.Properties as NatProps
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
 open import Relation.Binary.Definitions
+open import Relation.Nullary using (Dec; ¬_)
 open import Data.Nat as Nat using (ℕ; _≤_)
-open import Data.Product using (_×_; _,_)
+open import Data.Product using (_×_; Σ; _,_)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Agda.Primitive using (lsuc; Level)
-
-open import NatMap using (NatMap)
+open import Chain using (Chain; Height)
 
 record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
     field
@@ -16,6 +16,10 @@ record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
         ≈-sym : {a b : A} → a ≈ b → b ≈ a
         ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c
 
+record IsDecidable {a} (A : Set a) (R : A → A → Set a) : Set a where
+    field
+        R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
+
 record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where
@@ -48,6 +52,24 @@ record IsLattice {a} (A : Set a)
         ; ⊔-idemp to ⊓-idemp
         )
 
+record IsFiniteHeightLattice {a} (A : Set a)
+    (h : ℕ)
+    (_≈_ : A → A → Set a)
+    (_⊔_ : A → A → A)
+    (_⊓_ : A → A → A) : Set (lsuc a) where
+
+    _≼_ : A → A → Set a
+    a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)
+
+    _≺_ : A → A → Set a
+    a ≺ b = (a ≼ b) × (¬ a ≈ b)
+
+    field
+        isLattice : IsLattice A _≈_ _⊔_ _⊓_
+        fixedHeight : Height _≺_ h
+
+    open IsLattice isLattice public
+
 record Semilattice {a} (A : Set a) : Set (lsuc a) where
     field
         _≈_ : A → A → Set a