From 45f2babfa390ad860d7ecd11bd5bf9de85dd79cd Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 11 Feb 2024 15:37:00 -0800
Subject: [PATCH] Fix typo in FixedHeightLattice definition

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

diff --git a/Lattice.agda b/Lattice.agda
index 353e8d5..54d6dbc 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -153,6 +153,6 @@ record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
         _⊔_ : A → A → A
         _⊓_ : A → A → A
 
-        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊔_
+        isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
 
     open IsFiniteHeightLattice isFiniteHeightLattice public