move maxLUB and minGLB to Data.Nat.Order, remove unnecessary imports

Author: LorenzoMolena

Cubical/Data/Nat/Order.agda

@@ -277,6 +277,20 @@ min-≤-right {zero} {n} = zero-≤
 min-≤-right {suc m} {zero} = ≤-refl
 min-≤-right {suc m} {suc n} = subst (_≤ _) (sym minSuc) $ suc-≤-suc $ min-≤-right {m} {n}
 
+maxLUB : ∀ {x} → m ≤ x → n ≤ x → max m n ≤ x
+maxLUB {zero}  {n}     _    n≤x  = n≤x
+maxLUB {suc m} {zero}  sm≤x _    = sm≤x
+maxLUB {suc m} {suc n} sm≤x sn≤x with m <ᵇ n
+... | false = sm≤x
+... | true  = sn≤x
+
+minGLB : ∀ {x} → x ≤ m → x ≤ n → x ≤ min m n
+minGLB {zero}  {n}     x≤0 _     = x≤0
+minGLB {suc m} {zero}  _   x≤0   = x≤0
+minGLB {suc m} {suc n} x≤sm x≤sn with m <ᵇ n
+... | false = x≤sn
+... | true  = x≤sm
+
 -- Boolean order relations and their conversions to/from ≤ and <
 
 _≤ᵇ_ : ℕ → ℕ → Bool

Cubical/Relation/Binary/Order/Pseudolattice/Instances/Int.agda

@@ -8,8 +8,6 @@ open import Cubical.Data.Int.Order renaming (_≤_ to _≤ℤ_)
 open import Cubical.Relation.Binary.Order.Poset.Instances.Int
 open import Cubical.Relation.Binary.Order.Pseudolattice
 
-open PseudolatticeStr
-
 ℤ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
 ℤ≤Pseudolattice = makePseudolatticeFromPoset ℤ≤Poset min max
   min≤

Cubical/Relation/Binary/Order/Pseudolattice/Instances/Nat.agda

@@ -2,31 +2,12 @@ module Cubical.Relation.Binary.Order.Pseudolattice.Instances.Nat where
 
 open import Cubical.Foundations.Prelude
 
-open import Cubical.Data.Bool.Base
-
 open import Cubical.Data.Nat
 open import Cubical.Data.Nat.Order renaming (_≤_ to _≤ℕ_)
 
 open import Cubical.Relation.Binary.Order.Poset.Instances.Nat
 open import Cubical.Relation.Binary.Order.Pseudolattice
 
-open PseudolatticeStr
-
-private
-  minGLB : ∀ {m n x} → x ≤ℕ m → x ≤ℕ n → x ≤ℕ min m n
-  minGLB {zero}  {n}     x≤0 _     = x≤0
-  minGLB {suc m} {zero}  _   x≤0   = x≤0
-  minGLB {suc m} {suc n} x≤sm x≤sn with m <ᵇ n
-  ... | false = x≤sn
-  ... | true  = x≤sm
-
-  maxLUB : ∀ {m n x} → m ≤ℕ x → n ≤ℕ x → max m n ≤ℕ x
-  maxLUB {zero}  {n}     _    n≤x  = n≤x
-  maxLUB {suc m} {zero}  sm≤x _    = sm≤x
-  maxLUB {suc m} {suc n} sm≤x sn≤x with m <ᵇ n
-  ... | false = sm≤x
-  ... | true  = sn≤x
-
 ℕ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
 ℕ≤Pseudolattice = makePseudolatticeFromPoset ℕ≤Poset min max
   min-≤-left