Merge branch 'master' into divisibility

src/Algebra/Module/Bundles.agda

@@ -26,15 +26,15 @@
 module Algebra.Module.Bundles where
 
 open import Algebra.Bundles
-  using (Semiring; Ring; CommutativeSemiring; CommutativeRing;
-  CommutativeMonoid; AbelianGroup)
+  using (Semiring; Ring; CommutativeSemiring; CommutativeRing
+        ; CommutativeMonoid; AbelianGroup)
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions using (Involutive)
 import Algebra.Module.Bundles.Raw as Raw
 open import Algebra.Module.Core using (Opₗ; Opᵣ)
 open import Algebra.Module.Structures
-  using (IsLeftSemimodule; IsRightSemimodule; IsBisemimodule;
-  IsSemimodule; IsLeftModule; IsRightModule; IsModule; IsBimodule)
+  using (IsLeftSemimodule; IsRightSemimodule; IsBisemimodule
+        ; IsSemimodule; IsLeftModule; IsRightModule; IsModule; IsBimodule)
 open import Algebra.Module.Definitions
 open import Function.Base using (flip)
 open import Level using (Level; _⊔_; suc)

src/Algebra/Module/Structures.agda

@@ -18,8 +18,8 @@ open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Module.Core  using (Opₗ; Opᵣ)
 import Algebra.Definitions as Defs
 open import Algebra.Module.Definitions
-  using (module LeftDefs; module RightDefs; module BiDefs;
-  module SimultaneousBiDefs)
+  using (module LeftDefs; module RightDefs; module BiDefs
+        ; module SimultaneousBiDefs)
 open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (Level; _⊔_)

src/Algebra/Morphism/Bundles.agda

@@ -10,7 +10,10 @@
 
 module Algebra.Morphism.Bundles where
 
-open import Algebra.Bundles.Raw
+open import Algebra.Bundles.Raw using
+  ( RawMagma; RawMonoid; RawGroup; RawQuasigroup; RawLoop
+  ; RawSemiring; RawNearSemiring; RawKleeneAlgebra
+  ; RawRingWithoutOne; RawRing)
 open import Algebra.Morphism.Structures
 open import Level using (Level; suc; _⊔_)
 --open import Relation.Binary.Morphism using (IsRelHomomorphism)

src/Algebra/Morphism/Consequences.agda

@@ -9,10 +9,11 @@
 module Algebra.Morphism.Consequences where
 
 open import Algebra using (Magma)
-open import Algebra.Morphism.Definitions
+open import Algebra.Morphism.Definitions using (Homomorphic₂)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_)
 open import Function.Definitions
+  using (Injective; Congruent; Inverseᵇ; Inverseˡ)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------

src/Algebra/Morphism/Construct/Composition.agda

@@ -14,7 +14,7 @@ open import Algebra.Morphism.Structures
 open import Function.Base using (_∘_)
 import Function.Construct.Composition as Func
 open import Level using (Level)
-open import Relation.Binary.Morphism.Construct.Composition
+open import Relation.Binary.Morphism.Construct.Composition using (isRelHomomorphism)
 open import Relation.Binary.Definitions using (Transitive)
 
 private

src/Algebra/Morphism/Construct/Initial.agda

@@ -16,9 +16,9 @@ module Algebra.Morphism.Construct.Initial {c ℓ : Level} where
 
 open import Algebra.Bundles.Raw using (RawMagma)
 open import Algebra.Morphism.Structures
+  using (IsMagmaHomomorphism; IsMagmaMonomorphism)
 open import Function.Definitions using (Injective)
 import Relation.Binary.Morphism.Definitions as Rel
-open import Relation.Binary.Morphism.Structures
 open import Relation.Binary.Core using (Rel)
 
 open import Algebra.Construct.Initial {c} {ℓ}

src/Algebra/Morphism/Construct/Terminal.agda

@@ -18,11 +18,13 @@ module Algebra.Morphism.Construct.Terminal {c ℓ : Level} where
 open import Algebra.Bundles.Raw
   using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
 open import Algebra.Morphism.Structures
-
+  using(IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism
+        ; IsNearSemiringHomomorphism; IsSemiringHomomorphism
+        ; IsRingHomomorphism)
 open import Data.Product.Base using (_,_)
 open import Function.Definitions using (StrictlySurjective)
 import Relation.Binary.Morphism.Definitions as Rel
-open import Relation.Binary.Morphism.Structures
+open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism)
 
 open import Algebra.Construct.Terminal {c} {ℓ}
 

src/Algebra/Morphism/GroupMonomorphism.agda

@@ -9,9 +9,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles
+open import Algebra.Bundles using (RawGroup)
 open import Algebra.Morphism.Structures
-open import Relation.Binary.Core
+  using (IsGroupMonomorphism; IsMonoidMonomorphism)
+open import Function.Base using (_∘_)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Morphism.GroupMonomorphism
   {a b ℓ₁ ℓ₂} {G₁ : RawGroup a ℓ₁} {G₂ : RawGroup b ℓ₂} {⟦_⟧}
@@ -25,7 +29,9 @@ open RawGroup G₂ renaming
   (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
 
 open import Algebra.Definitions
+  using (Inverse; LeftInverse; RightInverse; Congruent₁)
 open import Algebra.Structures
+  using (IsMagma; IsGroup; IsAbelianGroup)
 open import Data.Product.Base using (_,_)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 

src/Algebra/Morphism/MagmaMonomorphism.agda

@@ -9,10 +9,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
-open import Algebra.Bundles
-open import Algebra.Morphism.Structures
-open import Relation.Binary.Core
+open import Algebra.Bundles using (RawMagma)
+open import Algebra.Morphism.Structures using (IsMagmaMonomorphism)
 
 module Algebra.Morphism.MagmaMonomorphism
   {a b ℓ₁ ℓ₂} {M₁ : RawMagma a ℓ₁} {M₂ : RawMagma b ℓ₂} {⟦_⟧}
@@ -24,11 +22,15 @@ open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
 open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
 
 open import Algebra.Structures
+  using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma)
 open import Algebra.Definitions
+  using (Congruent₂; Associative; Commutative; Idempotent ; Selective
+        ; LeftCancellative; RightCancellative; Cancellative)
 open import Data.Product.Base using (map)
 open import Data.Sum.Base using (inj₁; inj₂)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
+open import Relation.Binary.Core using (Rel)
 
 ------------------------------------------------------------------------
 -- Properties

src/Algebra/Morphism/MonoidMonomorphism.agda

@@ -9,9 +9,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles
-open import Algebra.Morphism.Structures
-open import Relation.Binary.Core
+open import Algebra.Bundles using (RawMonoid)
+open import Algebra.Morphism.Structures using (IsMonoidMonomorphism)
 
 module Algebra.Morphism.MonoidMonomorphism
   {a b ℓ₁ ℓ₂} {M₁ : RawMonoid a ℓ₁} {M₂ : RawMonoid b ℓ₂} {⟦_⟧}
@@ -23,8 +22,11 @@ open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; 
 open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)
 
 open import Algebra.Definitions
+  using (Identity; Zero; LeftIdentity; RightIdentity; LeftZero; RightZero)
 open import Algebra.Structures
+  using (IsMagma; IsMonoid; IsCommutativeMonoid)
 open import Data.Product.Base using (map)
+open import Relation.Binary.Core using (Rel)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------

src/Algebra/Morphism/RingMonomorphism.agda

@@ -9,11 +9,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles
-open import Algebra.Morphism.Structures
-import Algebra.Morphism.GroupMonomorphism  as GroupMonomorphism
-import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism
-open import Relation.Binary.Core
+open import Algebra.Bundles using (RawRing)
+open import Algebra.Morphism.Structures using (IsRingMonomorphism)
+
 
 module Algebra.Morphism.RingMonomorphism
   {a b ℓ₁ ℓ₂} {R₁ : RawRing a ℓ₁} {R₂ : RawRing b ℓ₂} {⟦_⟧}
@@ -25,9 +23,14 @@ open RawRing R₁ renaming (Carrier to A; _≈_ to _≈₁_)
 open RawRing R₂ renaming
   ( Carrier to B; _≈_ to _≈₂_; _+_ to _⊕_
   ; _*_ to _⊛_; 1# to 1#₂; 0# to 0#₂; -_ to ⊝_)
-
+import Algebra.Morphism.GroupMonomorphism  as GroupMonomorphism
+import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism
+open import Relation.Binary.Core using (Rel)
 open import Algebra.Definitions
+  using (_DistributesOverˡ_; _DistributesOverʳ_ ; _DistributesOver_
+        ; LeftZero; RightZero; Zero)
 open import Algebra.Structures
+  using (IsRing; IsCommutativeRing; IsGroup; IsMagma)
 open import Data.Product.Base using (proj₁; proj₂; _,_)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 

src/Algebra/Morphism/Structures.agda

@@ -8,13 +8,14 @@
 
 module Algebra.Morphism.Structures where
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Bundles
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Level using (Level; _⊔_)
-open import Function.Definitions
-open import Relation.Binary.Core
+open import Function.Definitions using (Injective; Surjective)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Morphism.Structures
+  using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism)
 
 private
   variable

src/Data/List/Membership/DecPropositional.agda

@@ -13,8 +13,6 @@ module Data.List.Membership.DecPropositional
 
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
-
 ------------------------------------------------------------------------
 -- Re-export contents of propositional membership
 

src/Data/List/Membership/Propositional/Properties/Core.agda

@@ -13,7 +13,7 @@
 module Data.List.Membership.Propositional.Properties.Core where
 
 open import Data.List.Base using (List; [])
-open import Data.List.Membership.Propositional
+open import Data.List.Membership.Propositional using (_∈_; _∉_; find; lose)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product.Base as Product using (_,_; ∃; _×_)
 open import Function.Base using (flip; id; _∘_)

src/Data/List/Membership/Propositional/Properties/WithK.agda

@@ -9,14 +9,15 @@
 
 module Data.List.Membership.Propositional.Properties.WithK where
 
-open import Level using (Level)
-open import Function.Bundles using (Equivalence)
-open import Data.List.Base
-open import Data.List.Relation.Unary.Unique.Propositional
-open import Data.List.Membership.Propositional
+open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
+open import Data.List.Membership.Propositional using (_∈_; _∉_)
 import Data.List.Membership.Setoid.Properties as Membership
+  using (unique⇒irrelevant)
 open import Data.List.Relation.Binary.BagAndSetEquality using (_∼[_]_; set; bag)
 open import Data.Product using (_,_)
+open import Function.Bundles using (Equivalence)
+open import Level using (Level)
 open import Relation.Unary using (Irrelevant)
 open import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)

src/Data/List/Nary/NonDependent.agda

@@ -12,8 +12,7 @@ open import Data.Nat.Base using (zero; suc)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Product.Base as Product using (_,_)
 open import Data.Product.Nary.NonDependent using (Product)
-open import Function.Base using ()
-open import Function.Nary.NonDependent.Base
+open import Function.Nary.NonDependent.Base using (Arrows; Sets; _<$>_)
 
 ------------------------------------------------------------------------
 -- n-ary smart constructors

src/Data/List/NonEmpty/Base.agda

@@ -12,12 +12,12 @@ open import Level using (Level)
 open import Data.Bool.Base using (Bool; false; true)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Maybe.Base using (Maybe ; nothing; just)
-open import Data.Nat.Base as ℕ
+open import Data.Nat.Base as ℕ using (ℕ; suc; zero; pred)
 open import Data.Product.Base as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-open import Function.Base
+open import Function.Base using (id; _∘′_; _∘_; const)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
 open import Relation.Unary using (Pred; Decidable; U; ∅)

src/Data/List/NonEmpty/Effectful.agda

@@ -8,14 +8,14 @@
 
 module Data.List.NonEmpty.Effectful where
 
-open import Agda.Builtin.List
+open import Data.List.Base using (List; []; _∷_)
 import Data.List.Effectful as List
 open import Data.List.NonEmpty.Base
 open import Data.Product.Base using (uncurry)
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Effect.Comonad
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad)
+open import Effect.Comonad using (RawComonad)
 open import Function.Base using (flip; _∘′_; _∘_)
 
 ------------------------------------------------------------------------

src/Data/List/NonEmpty/Effectful/Transformer.agda

@@ -9,13 +9,13 @@
 module Data.List.NonEmpty.Effectful.Transformer where
 
 open import Data.List.NonEmpty.Base as List⁺ using (List⁺; _∷_)
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Function.Base
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; RawMonadT)
+open import Function.Base using (_∘′_; _∘_; _$_)
 open import Level using (Level)
 
-import Data.List.NonEmpty.Effectful as List⁺
+import Data.List.NonEmpty.Effectful as List⁺ using (module TraversableM)
 
 private
   variable

src/Data/List/NonEmpty/Instances.agda

@@ -9,8 +9,9 @@
 module Data.List.NonEmpty.Instances where
 
 open import Data.List.NonEmpty.Effectful
+  using (functor; applicative; monad; comonad)
 import Data.List.NonEmpty.Effectful.Transformer as Trans
-
+  using (functor; applicative; monad; monadT)
 instance
   -- List⁺ instances
   nonEmptyListFunctor = functor

src/Data/List/NonEmpty/Relation/Unary/All.agda

@@ -12,7 +12,7 @@ import Data.List.Relation.Unary.All as List
 open import Data.List.Relation.Unary.All using ([]; _∷_)
 open import Data.List.Base using ([]; _∷_)
 open import Data.List.NonEmpty.Base using (List⁺; _∷_; toList)
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred)
 
 private

src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda

@@ -8,18 +8,19 @@
 
 module Data.List.Relation.Binary.Disjoint.Propositional.Properties where
 
-open import Level using (Level)
-open import Function.Base using (_∘_)
-open import Function.Bundles using (_⇔_)
-open import Data.List.Base
-open import Data.List.Relation.Binary.Disjoint.Propositional
-import Data.List.Relation.Unary.Any as Any
-open import Data.List.Relation.Unary.All as All
+
+open import Data.List.Base using (List; []; _∷_; concat; deduplicate)
+open import Data.List.Relation.Binary.Disjoint.Propositional using (Disjoint)
+import Data.List.Relation.Unary.Any as Any using (Any)
+open import Data.List.Relation.Unary.All as All using (All)
 open import Data.List.Relation.Unary.All.Properties using (¬Any⇒All¬)
 open import Data.List.Relation.Unary.Any.Properties using (++⁻)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.Product.Base as Product using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
+open import Function.Base using (_∘_)
+open import Function.Bundles using (_⇔_)
+open import Level using (Level)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (Symmetric; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)

src/Data/List/Relation/Binary/Disjoint/Setoid.agda

@@ -6,7 +6,6 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Binary.Disjoint.Setoid {c ℓ} (S : Setoid c ℓ) where
@@ -17,6 +16,7 @@ open import Function.Base using (_∘_)
 open import Data.List.Base using (List; []; [_]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.Product.Base using (_×_; _,_)
+open import Relation.Binary.Core using (Rel)
 
 open Setoid S renaming (Carrier to A)
 open import Data.List.Membership.Setoid S using (_∈_; _∉_)

src/Data/List/Relation/Binary/Equality/Propositional.agda

@@ -17,7 +17,7 @@ module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where
 open import Data.List.Base
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
-import Relation.Binary.PropositionalEquality.Properties as ≡
+import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 
 ------------------------------------------------------------------------
 -- Re-export everything from setoid equality