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