Tighten imports, last big versoin (#2347)

* more tightening of imports. Mostly driven by Data.Bool, Data.Nat and Data.Char.

* more tightening of imports

* mostly Data.Unit

* slightly tighten imports.

* remove import of unused Lift)

* fix all 3 things noticed by @jamesmckinna

Author: JacquesCarette

src/Algebra/Construct/LexProduct.agda

@@ -6,16 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Data.Bool using (true; false)
+open import Algebra.Bundles using (Magma)
+open import Algebra.Definitions
+open import Data.Bool.Base using (true; false)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (¬_; does; yes; no)
-open import Relation.Nullary.Negation using (contradiction; contradiction₂)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Construct.LexProduct

src/Algebra/Properties/Monoid/Sum.agda

@@ -7,16 +7,17 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Monoid)
+
+module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
+
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
-open import Data.Vec.Functional as Vector
+open import Data.Vec.Functional as Vector using (Vector; replicate; init;
+  last; head; tail)
 open import Data.Fin.Base using (zero; suc)
-open import Data.Unit using (tt)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≗_; _≡_)
 
-module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
-
 open Monoid M
   renaming
   ( _∙_       to _+_

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (IdempotentCommutativeMonoid)
 
 open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
 open import Data.Fin.Base using (Fin; zero; suc)

src/Codata/Sized/Conat/Literals.agda

@@ -8,9 +8,9 @@
 
 module Codata.Sized.Conat.Literals where
 
-open import Agda.Builtin.FromNat
-open import Data.Unit
-open import Codata.Sized.Conat
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Unit.Base using (⊤)
+open import Codata.Sized.Conat using (Conat; fromℕ)
 
 number : ∀ {i} → Number (Conat i)
 number = record

src/Codata/Sized/Delay/Properties.agda

@@ -10,7 +10,7 @@ module Codata.Sized.Delay.Properties where
 
 open import Size
 import Data.Sum.Base as Sum
-import Data.Nat as ℕ
+import Data.Nat.Base as ℕ
 open import Codata.Sized.Thunk using (Thunk; force)
 open import Codata.Sized.Conat
 open import Codata.Sized.Conat.Bisimilarity as Coℕ using (zero ; suc)

src/Data/Container/Fixpoints/Sized.agda

@@ -8,10 +8,10 @@
 
 module Data.Container.Fixpoints.Sized where
 
-open import Level
-open import Size
-open import Codata.Sized.M
-open import Data.W.Sized
+open import Level using (Level; _⊔_)
+open import Size using (Size)
+open import Codata.Sized.M using (M)
+open import Data.W.Sized using (W)
 open import Data.Container hiding (μ) public
 
 private

src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda

@@ -11,7 +11,7 @@ module Data.Container.Indexed.Relation.Binary.Pointwise.Properties where
 open import Axiom.Extensionality.Propositional
 open import Data.Container.Indexed.Core
 open import Data.Container.Indexed.Relation.Binary.Pointwise
-open import Data.Product using (_,_; Σ-syntax; -,_)
+open import Data.Product.Base using (_,_; Σ-syntax; -,_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P

src/Data/Fin/Permutation.agda

@@ -8,7 +8,7 @@
 
 module Data.Fin.Permutation where
 
-open import Data.Bool using (true; false)
+open import Data.Bool.Base using (true; false)
 open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns

src/Data/Fin/Properties.agda

@@ -22,7 +22,7 @@ open import Data.Nat.Base as ℕ
   using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; s<s⁻¹; _∸_; _^_)
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
-open import Data.Unit using (⊤; tt)
+open import Data.Unit.Base using (⊤; tt)
 open import Data.Product.Base as Product
   using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
 open import Data.Product.Properties using (,-injective)

src/Data/Fin/Substitution/Lemmas.agda

@@ -9,19 +9,19 @@
 module Data.Fin.Substitution.Lemmas where
 
 open import Data.Fin.Substitution
-open import Data.Nat hiding (_⊔_; _/_)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Fin.Base using (Fin; zero; suc; lift)
-open import Data.Vec.Base
+open import Data.Vec.Base using (lookup; []; _∷_; map)
 import Data.Vec.Properties as Vec
 open import Function.Base as Fun using (_∘_; _$_; flip)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; sym; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_; _▻_)
 open ≡-Reasoning
-open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred)
 
 private

src/Data/Integer.agda

@@ -31,7 +31,7 @@ open import Data.Integer.Properties public
 -- Show
 
 import Data.Nat.Show as ℕ using (show)
-open import Data.Sign as Sign using (Sign)
+open import Data.Sign.Base as Sign using (Sign)
 open import Data.String.Base using (String; _++_)
 
 show : ℤ → String

src/Data/Integer/DivMod.agda

@@ -13,7 +13,6 @@ open import Data.Integer.Properties
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z<s; s<s)
 import Data.Nat.Properties as ℕ
 import Data.Nat.DivMod as ℕ
-import Data.Sign as S
 open import Function.Base using (_∘′_)
 open import Relation.Nullary.Decidable
 open import Relation.Binary.PropositionalEquality

src/Data/Integer/Divisibility/Signed.agda

@@ -16,7 +16,7 @@ import Data.Nat.Base as ℕ
 import Data.Nat.Divisibility as ℕ
 import Data.Nat.Coprimality as ℕ
 import Data.Nat.Properties as ℕ
-import Data.Sign as Sign
+import Data.Sign.Base as Sign
 import Data.Sign.Properties as Sign
 open import Level
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_)

src/Data/Integer/Literals.agda

@@ -8,9 +8,9 @@
 
 module Data.Integer.Literals where
 
-open import Agda.Builtin.FromNat
-open import Agda.Builtin.FromNeg
-open import Data.Unit using (⊤)
+open import Agda.Builtin.FromNat using (Number)
+open import Agda.Builtin.FromNeg using (Negative)
+open import Data.Unit.Base using (⊤)
 open import Data.Integer.Base using (ℤ; -_; +_)
 
 number : Number ℤ

src/Data/Integer/Properties.agda

@@ -23,7 +23,7 @@ import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
 open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Data.Sign as Sign using (Sign)
+open import Data.Sign.Base as Sign using (Sign)
 import Data.Sign.Properties as Sign
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)

src/Data/Integer/Tactic/RingSolver.agda

@@ -16,7 +16,7 @@ open import Data.Maybe.Base using (just; nothing)
 open import Data.Integer.Base
 open import Data.Integer.Properties
 open import Level using (0ℓ)
-open import Data.Unit using (⊤)
+open import Data.Unit.Base using (⊤)
 open import Relation.Binary.PropositionalEquality
 import Tactic.RingSolver as Solver
 import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR

src/Data/List/Fresh/Properties.agda

@@ -8,7 +8,7 @@
 
 module Data.List.Fresh.Properties where
 
-open import Level using (Level; _⊔_; Lift)
+open import Level using (Level; _⊔_)
 open import Data.Product.Base using (_,_)
 open import Relation.Nullary
 open import Relation.Unary as U using (Pred)

src/Data/List/Literals.agda

@@ -8,10 +8,10 @@
 
 module Data.List.Literals where
 
-open import Agda.Builtin.FromString
-open import Data.Unit
-open import Agda.Builtin.Char
-open import Agda.Builtin.List
+open import Agda.Builtin.FromString using (IsString)
+open import Data.Unit.Base using (⊤)
+open import Agda.Builtin.Char using (Char)
+open import Agda.Builtin.List using (List)
 open import Data.String.Base using (toList)
 
 isString : IsString (List Char)

src/Data/List/NonEmpty/Properties.agda

@@ -12,7 +12,7 @@ open import Effect.Monad
 open import Data.Nat
 open import Data.Nat.Properties
 open import Data.Maybe.Properties using (just-injective)
-open import Data.Bool using (Bool; true; false)
+open import Data.Bool.Base using (Bool; true; false)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Effectful using () renaming (monad to listMonad)
 open import Data.List.NonEmpty.Effectful using () renaming (monad to list⁺Monad)

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -30,7 +30,7 @@ import Data.List.Relation.Unary.Unique.Setoid as Unique
 import Data.List.Membership.Setoid as Membership
 open import Data.List.Membership.Setoid.Properties using (∈-∃++; ∈-insert)
 import Data.List.Properties as Lₚ
-open import Data.Nat hiding (_⊔_)
+open import Data.Nat.Base using (ℕ; suc; _<_; z<s; _+_)
 open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)

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

@@ -25,7 +25,7 @@ import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset
 open import Data.List.Relation.Binary.Subset.Propositional
 open import Data.List.Relation.Binary.Permutation.Propositional
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
-open import Data.Nat using (ℕ; _≤_)
+open import Data.Nat.Base using (ℕ; _≤_)
 import Data.Product.Base as Product
 import Data.Sum.Base as Sum
 open import Effect.Monad

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -20,20 +20,19 @@ open import Data.List.Membership.Propositional.Properties.Core
   using (Any↔; find∘map; map∘find; lose∘find)
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise; []; _∷_)
-open import Data.Nat using (zero; suc; _<_; z<s; s<s; s≤s)
+open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s; s≤s)
 open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; m<n⇒m<1+n)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any as MAny using (just)
 open import Data.Product.Base as Product
   using (_×_; _,_; ∃; ∃₂; proj₁; proj₂; uncurry′)
-open import Data.Product.Properties
 open import Data.Product.Function.NonDependent.Propositional
   using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
-open import Effect.Monad
-open import Function.Base
+open import Effect.Monad using (RawMonad)
+open import Function.Base using (_$_; _∘_; flip; const; id; _∘′_)
 open import Function.Bundles
 import Function.Properties.Inverse as Inverse
 open import Function.Related.Propositional as Related using (Kind; Related)

src/Data/List/Relation/Unary/Grouped/Properties.agda

@@ -8,20 +8,20 @@
 
 module Data.List.Relation.Unary.Grouped.Properties where
 
-open import Data.Bool using (true; false)
+open import Data.Bool.Base using (true; false)
 open import Data.List.Base using ([]; [_]; _∷_; map; derun)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _∷_)
 open import Data.List.Relation.Unary.Grouped
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_; _on_)
+open import Level using (Level)
 open import Relation.Binary.Definitions as B
 open import Relation.Binary.Core using (_⇔_; REL; Rel)
 open import Relation.Unary as U using (Pred)
-open import Relation.Nullary using (¬_; does; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
-open import Level
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable

src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda

@@ -6,17 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
-import Data.List.Relation.Unary.Unique.DecSetoid.Properties as Setoid
-open import Data.List.Relation.Unary.All.Properties using (all-filter)
-open import Level
 open import Relation.Binary.Definitions using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 module Data.List.Relation.Unary.Unique.DecPropositional.Properties
   {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
+open import Data.List.Base using (deduplicate)
+open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.DecPropositional _≟_
+import Data.List.Relation.Unary.Unique.DecSetoid.Properties as Setoid
+open import Level
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 ------------------------------------------------------------------------
 -- Re-export propositional properties

src/Data/List/Sort/MergeSort.agda

@@ -10,8 +10,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Bool using (true; false)
+open import Relation.Binary.Bundles using (DecTotalOrder)
+
+module Data.List.Sort.MergeSort
+  {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
+open import Data.Bool.Base using (true; false)
 open import Data.List.Base
+  using (List; []; _∷_; merge; length; map; [_]; concat; _++_)
 open import Data.List.Properties using (length-partition; ++-assoc; concat-[-])
 open import Data.List.Relation.Unary.Linked using ([]; [-])
 import Data.List.Relation.Unary.Sorted.TotalOrder.Properties as Sorted
@@ -20,17 +25,13 @@ import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Binary.Permutation.Propositional
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
 open import Data.Maybe.Base using (just)
-open import Relation.Nullary.Decidable using (does)
 open import Data.Nat.Base using (_<_; _>_; z<s; s<s)
 open import Data.Nat.Induction
 open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product.Base as Product using (_,_)
 open import Function.Base using (_∘_)
-open import Relation.Binary.Bundles using (DecTotalOrder)
-open import Relation.Nullary.Negation using (¬_)
-
-module Data.List.Sort.MergeSort
-  {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core using (does)
 
 open DecTotalOrder O renaming (Carrier to A)
 

src/Data/Maybe.agda

@@ -9,10 +9,10 @@
 module Data.Maybe where
 
 open import Data.Empty using (⊥)
-open import Data.Unit using (⊤)
+open import Data.Unit.Base using (⊤)
 open import Data.Bool.Base using (T)
-open import Data.Maybe.Relation.Unary.All
-open import Data.Maybe.Relation.Unary.Any
+open import Data.Maybe.Relation.Unary.All using (All)
+open import Data.Maybe.Relation.Unary.Any using (Any; just)
 open import Level using (Level)
 
 private

src/Data/Nat/Combinatorics/Specification.agda

@@ -10,7 +10,7 @@
 
 module Data.Nat.Combinatorics.Specification where
 
-open import Data.Bool using (T; true; false)
+open import Data.Bool.Base using (T; true; false)
 open import Data.Nat.Base
 open import Data.Nat.DivMod
 open import Data.Nat.Divisibility

src/Data/Nat/Literals.agda

@@ -8,9 +8,9 @@
 
 module Data.Nat.Literals where
 
-open import Agda.Builtin.FromNat
-open import Agda.Builtin.Nat
-open import Data.Unit
+open import Agda.Builtin.FromNat using (Number)
+open import Agda.Builtin.Nat using (Nat)
+open import Data.Unit.Base using (⊤)
 
 number : Number Nat
 number = record

src/Data/Nat/Logarithm.agda

@@ -8,7 +8,7 @@
 
 module Data.Nat.Logarithm where
 
-open import Data.Nat
+open import Data.Nat.Base
 open import Data.Nat.Induction using (<-wellFounded)
 open import Data.Nat.Logarithm.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)