From 561d0f343ad8a7335ae3bd7b458c2628a874e377 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 20 Aug 2023 19:57:26 -0700
Subject: [PATCH] Move < definition to Semilattice

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

diff --git a/Lattice.agda b/Lattice.agda
index 132ad0f..af572aa 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -24,6 +24,12 @@ record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where
 
+    _≼_ : A → A → Set a
+    a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)
+
+    _≺_ : A → A → Set a
+    a ≺ b = (a ≼ b) × (¬ a ≈ b)
+
     field
         ≈-equiv : IsEquivalence A _≈_
 
@@ -46,7 +52,7 @@ record IsLattice {a} (A : Set a)
         absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
 
     open IsSemilattice joinSemilattice public
-    open IsSemilattice meetSemilattice public hiding (≈-equiv; ≈-refl; ≈-sym; ≈-trans) renaming
+    open IsSemilattice meetSemilattice public using () renaming
         ( ⊔-assoc to ⊓-assoc
         ; ⊔-comm to ⊓-comm
         ; ⊔-idemp to ⊓-idemp
@@ -58,15 +64,9 @@ record IsFiniteHeightLattice {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
+        fixedHeight : Height (IsLattice._≺_ isLattice) h
 
     open IsLattice isLattice public