[imports] Algebra.Bundles .. Algebra.Consequences.* (#2596)

* Algebra Bundles Consequences

* Algebra Bundles Consequences

* space

* lines

* cleaning import

Author: jmougeot

src/Algebra/Bundles/Raw.agda

@@ -8,7 +8,7 @@
 
 module Algebra.Bundles.Raw where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles.Raw using (RawSetoid)
 open import Level using (suc; _⊔_)

src/Algebra/Consequences/Base.agda

@@ -10,10 +10,11 @@
 module Algebra.Consequences.Base
   {a} {A : Set a} where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions
-open import Data.Sum.Base
-open import Relation.Binary.Core
+  using (Selective; Idempotent; SelfInverse; Involutive)
+open import Data.Sum.Base using (_⊎_; reduce)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive)
 
 module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where

src/Algebra/Consequences/Propositional.agda

@@ -19,8 +19,8 @@ open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
 open import Relation.Unary using (Pred)
+open import Algebra.Core using (Op₁; Op₂)
 
-open import Algebra.Core
 open import Algebra.Definitions {A = A} _≡_
 import Algebra.Consequences.Setoid (setoid A) as Base
 

src/Algebra/Consequences/Setoid.agda

@@ -7,7 +7,6 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions
   using (Substitutive; Symmetric; Total)
@@ -22,6 +21,7 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
 import Relation.Binary.Consequences as Bin
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Reasoning.Setoid S
 open import Relation.Unary using (Pred)