end construct import cleaning (#2600)

* end construct import

* cleaning import

Author: jmougeot

src/Algebra/Construct/Initial.agda

@@ -21,7 +21,7 @@ open import Algebra.Bundles.Raw
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Congruent₂)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
-open import Data.Empty.Polymorphic
+open import Data.Empty.Polymorphic using (⊥)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.Definitions

src/Algebra/Construct/LiftedChoice.agda

@@ -10,7 +10,7 @@ open import Algebra
 
 module Algebra.Construct.LiftedChoice where
 
-open import Algebra.Consequences.Base
+open import Algebra.Consequences.Base using (sel⇒idem)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
 open import Data.Product.Base using (_×_; _,_)
 open import Function.Base using (const; _$_)

src/Algebra/Construct/Pointwise.agda

@@ -17,7 +17,7 @@ open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Structures
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘′_; const)
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)

src/Algebra/Construct/Subst/Equality.agda

@@ -10,7 +10,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Data.Product.Base as Product
-open import Relation.Binary.Core
+open import Relation.Binary.Core using (Rel; _⇔_)
 
 module Algebra.Construct.Subst.Equality
   {a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂}
@@ -20,7 +20,7 @@ module Algebra.Construct.Subst.Equality
 open import Algebra.Definitions
 open import Algebra.Structures
 import Data.Sum.Base as Sum
-open import Function.Base
+open import Function.Base using (id; _∘_)
 open import Relation.Binary.Construct.Subst.Equality equiv
 
 ------------------------------------------------------------------------

src/Algebra/Construct/Terminal.agda

@@ -15,7 +15,7 @@ open import Level using (Level)
 module Algebra.Construct.Terminal {c ℓ : Level} where
 
 open import Algebra.Bundles
-open import Data.Unit.Polymorphic
+open import Data.Unit.Polymorphic using (⊤)
 open import Relation.Binary.Core using (Rel)
 
 ------------------------------------------------------------------------

src/Algebra/Construct/Zero.agda

@@ -19,10 +19,8 @@ open import Level using (Level)
 
 module Algebra.Construct.Zero {c ℓ : Level} where
 
-open import Algebra.Bundles.Raw
-  using (RawMagma)
-open import Algebra.Bundles
-  using (Magma; Semigroup; Band)
+open import Algebra.Bundles.Raw using (RawMagma)
+open import Algebra.Bundles using (Magma; Semigroup; Band)
 
 ------------------------------------------------------------------------
 -- Re-export those algebras which are both initial and terminal