From 8eaec3facd262b99531fd0db67b6a43e43afa292 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 23 Sep 2023 16:20:58 -0700 Subject: [PATCH] Provide a 'fixed height' predicate from Lattice for convenience Signed-off-by: Danila Fedorin --- Lattice.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Lattice.agda b/Lattice.agda index bdd6a35..4d08965 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -77,6 +77,9 @@ record IsLattice {a} (A : Set a) ; ≼-refl to ≽-refl ) + FixedHeight : ∀ (h : ℕ) → Set a + FixedHeight h = Chain.Height (_≈_) ≈-equiv _≺_ ≺-cong h + record IsFiniteHeightLattice {a} (A : Set a) (h : ℕ) (_≈_ : A → A → Set a) @@ -85,10 +88,11 @@ record IsFiniteHeightLattice {a} (A : Set a) field isLattice : IsLattice A _≈_ _⊔_ _⊓_ - fixedHeight : Chain.Height (_≈_) (IsLattice.≈-equiv isLattice) (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) h open IsLattice isLattice public + field + fixedHeight : FixedHeight h module _ {a b} {A : Set a} {B : Set b} (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where