[imports] Algebra.Lattice.Construct.* (#2603)

* Cleaning import Lattice 2

* t

* fix

Author: jmougeot

src/Algebra/Lattice/Construct/DirectProduct.agda

@@ -13,15 +13,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Algebra.Lattice
+module Algebra.Lattice.Construct.DirectProduct where
+
+open import Algebra using (Band)
+open import Algebra.Lattice using (Semilattice)
 import Algebra.Construct.DirectProduct as DirectProduct
 open import Data.Product.Base using (_,_; _<*>_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level; _⊔_)
 
-module Algebra.Lattice.Construct.DirectProduct where
-
 private
   variable
     a b ℓ₁ ℓ₂ : Level

src/Algebra/Lattice/Construct/LiftedChoice.agda

@@ -6,15 +6,16 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
+module Algebra.Lattice.Construct.LiftedChoice where
+
 open import Algebra
-open import Algebra.Lattice
-open import Algebra.Construct.LiftedChoice
+  using (Op₂; IsSelectiveMagma; Associative; Commutative)
+open import Algebra.Lattice.Structures using (IsSemilattice)
+open import Algebra.Construct.LiftedChoice using (Lift; isBand; comm)
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Level using (Level)
 
-module Algebra.Lattice.Construct.LiftedChoice where
-
 private
   variable
     a b p ℓ : Level

src/Algebra/Lattice/Construct/Subst/Equality.agda

@@ -9,18 +9,18 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core using (Op₂)
-open import Algebra.Definitions
-open import Algebra.Lattice.Structures
 open import Data.Product.Base using (_,_)
-open import Function.Base
-open import Relation.Binary.Core
+open import Relation.Binary.Core using (Rel ; _⇔_)
 
 module Algebra.Lattice.Construct.Subst.Equality
   {a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂}
   (equiv@(to , from) : ≈₁ ⇔ ≈₂)
   where
 
+open import Algebra.Core using (Op₂)
+open import Algebra.Lattice.Structures
+  using (IsSemilattice ;IsLattice ;IsDistributiveLattice ;IsBooleanAlgebra )
+open import Function.Base using (id)
 open import Algebra.Construct.Subst.Equality equiv
 open import Relation.Binary.Construct.Subst.Equality equiv
 

src/Algebra/Lattice/Construct/Zero.agda

@@ -17,8 +17,8 @@ open import Level using (Level)
 
 module Algebra.Lattice.Construct.Zero {c ℓ : Level} where
 
-open import Algebra.Lattice.Bundles
-open import Data.Unit.Polymorphic
+open import Algebra.Lattice.Bundles using (Semilattice)
+open import Data.Unit.Polymorphic using (⊤)
 
 ------------------------------------------------------------------------
 -- Bundles