Cleaning import Lattice 3 (#2605)

* Cleaning import Lattice 3

* Cleaning import Lattice 4

* t

Author: jmougeot

src/Algebra/Lattice/Morphism/Construct/Composition.agda

@@ -8,12 +8,14 @@
 
 module Algebra.Lattice.Morphism.Construct.Composition where
 
-open import Algebra.Lattice.Bundles
+open import Algebra.Lattice.Bundles using (RawLattice)
 open import Algebra.Lattice.Morphism.Structures
+  using (IsLatticeHomomorphism; IsLatticeIsomorphism; IsLatticeMonomorphism)
 open import Function.Base using (_∘_)
 import Function.Construct.Composition as Func
 open import Level using (Level)
 open import Relation.Binary.Morphism.Construct.Composition
+  using (isRelHomomorphism)
 open import Relation.Binary.Definitions using (Transitive)
 
 private

src/Algebra/Lattice/Morphism/Construct/Identity.agda

@@ -8,7 +8,7 @@
 
 module Algebra.Lattice.Morphism.Construct.Identity where
 
-open import Algebra.Lattice.Bundles
+open import Algebra.Lattice.Bundles using (RawLattice)
 open import Algebra.Lattice.Morphism.Structures
   using ( module LatticeMorphisms )
 open import Data.Product.Base using (_,_)

src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda

@@ -9,22 +9,23 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
 open import Algebra.Lattice
-open import Algebra.Lattice.Morphism.Structures
-import Algebra.Consequences.Setoid as Consequences
+  using (RawLattice; IsLattice; IsDistributiveLattice; isDistributiveLatticeʳʲᵐ)
+open import Algebra.Lattice.Morphism.Structures using (IsLatticeMonomorphism)
+
+module Algebra.Lattice.Morphism.LatticeMonomorphism
+  {a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
+  (isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧)
+  where
+
+open import Algebra using (Absorptive; _Absorbs_; _DistributesOverʳ_)
 import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
 import Algebra.Lattice.Properties.Lattice as LatticeProperties
 open import Data.Product.Base using (_,_; map)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
-module Algebra.Lattice.Morphism.LatticeMonomorphism
-  {a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
-  (isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧)
-  where
-
 open IsLatticeMonomorphism isLatticeMonomorphism
 open RawLattice L₁ renaming (_≈_ to _≈₁_; _∨_ to _∨_; _∧_ to _∧_)
 open RawLattice L₂ renaming (_≈_ to _≈₂_; _∨_ to _⊔_; _∧_ to _⊓_)

src/Algebra/Lattice/Morphism/Structures.agda

@@ -6,17 +6,16 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
-open import Algebra.Bundles
-open import Algebra.Morphism
-open import Algebra.Lattice.Bundles
+module Algebra.Lattice.Morphism.Structures where
+
+open import Algebra.Core using (Op₂)
+open import Algebra.Morphism using (module MagmaMorphisms)
+open import Algebra.Lattice.Bundles using (RawLattice)
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Level using (Level; _⊔_)
-open import Function.Definitions
-open import Relation.Binary.Morphism.Structures
-open import Relation.Binary.Core
-
-module Algebra.Lattice.Morphism.Structures where
+open import Function.Definitions using (Injective; Surjective)
+open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism)
+open import Relation.Binary.Core using (Rel)
 
 private
   variable

src/Algebra/Lattice/Properties/BooleanAlgebra.agda

@@ -15,11 +15,11 @@ module Algebra.Lattice.Properties.BooleanAlgebra
 open BooleanAlgebra B
 
 import Algebra.Lattice.Properties.DistributiveLattice as DistribLatticeProperties
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Structures _≈_
 open import Algebra.Definitions _≈_
 open import Algebra.Consequences.Setoid setoid
-open import Algebra.Bundles
+open import Algebra.Bundles using (CommutativeSemiring; CommutativeRing)
 open import Algebra.Lattice.Structures _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Function.Base using (id; _$_; _⟨_⟩_)

src/Algebra/Lattice/Properties/DistributiveLattice.agda

@@ -6,13 +6,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice.Bundles
-import Algebra.Lattice.Properties.Lattice as LatticeProperties
+open import Algebra.Lattice.Bundles using (DistributiveLattice)
 
 module Algebra.Lattice.Properties.DistributiveLattice
   {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
   where
 
+import Algebra.Lattice.Properties.Lattice as LatticeProperties
 open DistributiveLattice DL
 open import Algebra.Definitions _≈_
 open import Algebra.Lattice.Structures _≈_

src/Algebra/Lattice/Properties/Lattice.agda

@@ -6,21 +6,21 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice.Bundles
-import Algebra.Lattice.Properties.Semilattice as SemilatticeProperties
-open import Relation.Binary.Bundles using (Poset)
-import Relation.Binary.Lattice as R
-open import Function.Base
-open import Data.Product.Base using (_,_; swap)
+open import Algebra.Lattice.Bundles using (Lattice; Semilattice)
 
 module Algebra.Lattice.Properties.Lattice
   {l₁ l₂} (L : Lattice l₁ l₂) where
 
+import Algebra.Lattice.Properties.Semilattice as SemilatticeProperties
+open import Data.Product.Base using (_,_; swap)
 open Lattice L
-open import Algebra.Definitions _≈_
-open import Algebra.Structures _≈_
-open import Algebra.Lattice.Structures _≈_
+open import Algebra.Definitions _≈_ using (Idempotent; Congruent₂)
+open import Algebra.Structures _≈_ using (IsMagma; IsSemigroup; IsBand)
+open import Algebra.Lattice.Structures _≈_ using (IsLattice; IsSemilattice)
+open import Function.Base
 open import Relation.Binary.Reasoning.Setoid setoid
+open import Relation.Binary.Bundles using (Poset)
+import Relation.Binary.Lattice as R
 
 ------------------------------------------------------------------------
 -- _∧_ is a semilattice

src/Algebra/Lattice/Properties/Semilattice.agda

@@ -7,13 +7,13 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Lattice.Bundles using (Semilattice)
-open import Relation.Binary.Bundles using (Poset)
-import Relation.Binary.Lattice as B
-import Relation.Binary.Properties.Poset as PosetProperties
 
 module Algebra.Lattice.Properties.Semilattice
   {c ℓ} (L : Semilattice c ℓ) where
 
+open import Relation.Binary.Bundles using (Poset)
+import Relation.Binary.Lattice as B
+import Relation.Binary.Properties.Poset as PosetProperties
 open Semilattice L renaming (_∙_ to _∧_)
 
 open import Relation.Binary.Reasoning.Setoid setoid

src/Algebra/Lattice/Structures/Biased.agda

@@ -12,21 +12,27 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
-open import Algebra.Consequences.Setoid
-open import Data.Product.Base using (proj₁; proj₂)
-open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Lattice.Structures.Biased
   {a ℓ} {A : Set a}  -- The underlying set
   (_≈_ : Rel A ℓ)    -- The underlying equality relation
   where
 
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Consequences.Setoid
+  using (comm∧distrʳ⇒distr; distrib∧absorbs⇒distribˡ; comm∧distrˡ⇒distr;
+  comm∧invʳ⇒inv)
+open import Data.Product.Base using (proj₁; proj₂)
+open import Level using (_⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 open import Algebra.Definitions _≈_
+  using (Associative; Commutative; Congruent₁; RightInverse;
+  _DistributesOverʳ_; Absorptive)
 open import Algebra.Lattice.Structures _≈_
+  using (IsJoinSemilattice; IsMeetSemilattice; IsLattice;
+  IsDistributiveLattice; IsBooleanAlgebra)
 
 private
   variable