[ re #1993 ] Simplifying the dependency graph

Started with simplifying System.Console.ANSI
Noticed we could take advantage of Data.Product.Base

Author: gallais

src/Algebra/Construct/LexProduct/Base.agda

@@ -8,10 +8,10 @@
 
 open import Algebra.Core using (Op₂)
 open import Data.Bool.Base using (true; false)
-open import Data.Product using (_×_; _,_)
+open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (does; yes; no)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
 
 module Algebra.Construct.LexProduct.Base
   {a b ℓ} {A : Set a} {B : Set b}

src/Algebra/Lattice/Properties/Semilattice.agda

@@ -6,11 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Lattice
-open import Algebra.Structures
-open import Function
-open import Data.Product
-open import Relation.Binary
+open import Algebra.Lattice.Bundles using (Semilattice)
+open import Relation.Binary.Bundles using (Poset)
 import Relation.Binary.Lattice as B
 import Relation.Binary.Properties.Poset as PosetProperties
 

src/Codata/Sized/Cowriter.agda

@@ -16,9 +16,9 @@ open import Codata.Sized.Delay using (Delay; later; now)
 open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Unit.Base
 open import Data.List.Base using (List; []; _∷_)
-open import Data.List.NonEmpty using (List⁺; _∷_)
+open import Data.List.NonEmpty.Base using (List⁺; _∷_)
 open import Data.Nat.Base as Nat using (ℕ; zero; suc)
-open import Data.Product as Prod using (_×_; _,_)
+open import Data.Product.Base as Prod using (_×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤; _,_)

src/Codata/Sized/Stream.agda

@@ -15,10 +15,10 @@ open import Data.Nat.Base
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _∷⁺_)
 open import Data.Vec.Base using (Vec; []; _∷_)
-open import Data.Product as P hiding (map)
-open import Function.Base
+open import Data.Product.Base as P using (Σ; _×_; _,_; <_,_>; proj₁; proj₂)
+open import Function.Base using (id; _∘_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable

src/Data/Bool/Properties.agda

@@ -13,18 +13,18 @@ open import Algebra.Lattice.Bundles
 import Algebra.Lattice.Properties.BooleanAlgebra as BooleanAlgebraProperties
 open import Data.Bool.Base
 open import Data.Empty
-open import Data.Product
-open import Data.Sum.Base
-open import Function.Base
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
+open import Function.Base using (_⟨_⟩_; const; id)
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence
   using (_⇔_; equivalence; module Equivalence)
 open import Induction.WellFounded using (WellFounded; Acc; acc)
 open import Level using (Level; 0ℓ)
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality hiding ([_])
-open import Relation.Nullary using (ofʸ; ofⁿ; does; proof; yes; no)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
+open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_

src/Data/Digit.agda

@@ -9,21 +9,20 @@
 module Data.Digit where
 
 open import Data.Nat.Base
-open import Data.Nat.Properties
-open import Data.Nat.Solver
+open import Data.Nat.Properties using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n)
+open import Data.Nat.Solver using (module +-*-Solver)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ)
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Char using (Char)
+open import Data.Char.Base using (Char)
 open import Data.List.Base
-open import Data.Product
+open import Data.Product using (∃; _,_)
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
 open import Data.Nat.DivMod
 open import Data.Nat.Induction
-open import Relation.Nullary.Decidable using (does)
-open import Relation.Nullary.Decidable
-open import Relation.Binary using (Decidable)
+open import Relation.Nullary.Decidable using (True; does; toWitness)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
-open import Function
+open import Function.Base using (_$_)
 
 ------------------------------------------------------------------------
 -- Digits

src/Data/Fin/Base.agda

@@ -14,7 +14,7 @@ module Data.Fin.Base where
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
-open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)

src/Data/List/Base.agda

@@ -17,7 +17,7 @@ open import Data.Bool.Base as Bool
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
-open import Data.Product as Prod using (_×_; _,_; map₁; map₂′)
+open import Data.Product.Base as Prod using (_×_; _,_; map₁; map₂′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; const; flip)

src/Data/List/Fresh.agda

@@ -16,7 +16,7 @@ module Data.List.Fresh where
 open import Level using (Level; _⊔_)
 open import Data.Bool.Base using (true; false)
 open import Data.Unit.Polymorphic.Base using (⊤)
-open import Data.Product using (∃; _×_; _,_; -,_; proj₁; proj₂)
+open import Data.Product.Base using (∃; _×_; _,_; -,_; proj₁; proj₂)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)

src/Data/List/Fresh/NonEmpty.agda

@@ -11,9 +11,9 @@ module Data.List.Fresh.NonEmpty where
 open import Level using (Level; _⊔_)
 open import Data.List.Fresh as List# using (List#; []; cons; fresh)
 open import Data.Maybe.Base using (Maybe; nothing; just)
-open import Data.Nat using (ℕ; suc)
-open import Data.Product using (_×_; _,_)
-open import Relation.Binary as B using (Rel)
+open import Data.Nat.Base using (ℕ; suc)
+open import Data.Product.Base using (_×_; _,_)
+open import Relation.Binary.Core using (Rel)
 
 private
   variable

src/Data/List/Kleene/Base.agda

@@ -8,11 +8,12 @@
 
 module Data.List.Kleene.Base where
 
-open import Data.Product as Product using (_×_; _,_; map₂; map₁; proj₁; proj₂)
-open import Data.Nat     as ℕ       using (ℕ; suc; zero)
-open import Data.Maybe   as Maybe   using (Maybe; just; nothing)
-open import Data.Sum     as Sum     using (_⊎_; inj₁; inj₂)
-open import Level        as Level   using (Level)
+open import Data.Product.Base as Product
+  using (_×_; _,_; map₂; map₁; proj₁; proj₂)
+open import Data.Nat.Base as ℕ using (ℕ; suc; zero)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
+open import Level using (Level)
 
 open import Algebra.Core using (Op₂)
 open import Function.Base

src/Data/List/NonEmpty/Base.agda

@@ -14,7 +14,7 @@ open import Data.Bool.Properties using (T?)
 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.Product as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
+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; []; _∷_)

src/Data/List/Relation/Binary/Pointwise/Base.agda

@@ -8,9 +8,9 @@
 
 module Data.List.Relation.Binary.Pointwise.Base where
 
-open import Data.Product using (_×_; <_,_>)
+open import Data.Product.Base using (_×_; <_,_>)
 open import Data.List.Base using (List; []; _∷_)
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; _⇒_)
 
 private

src/Data/Maybe/Base.agda

@@ -14,7 +14,7 @@ open import Level
 open import Data.Bool.Base using (Bool; true; false; not)
 open import Data.Unit.Base using (⊤)
 open import Data.These.Base using (These; this; that; these)
-open import Data.Product as Prod using (_×_; _,_)
+open import Data.Product.Base as Prod using (_×_; _,_)
 open import Function.Base
 open import Relation.Nullary.Reflects
 open import Relation.Nullary.Decidable.Core

src/Data/Nat/Show.agda

@@ -16,9 +16,9 @@ open import Data.List.Effectful using (module TraversableA)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
 import Data.Maybe.Effectful as Maybe
 open import Data.Nat
-open import Data.Product using (proj₁)
-open import Data.String as String using (String)
-open import Function.Base
+open import Data.Product.Base using (proj₁)
+open import Data.String.Base as String using (String)
+open import Function.Base using (_∘′_; _∘_)
 open import Relation.Nullary.Decidable using (True)
 
 ------------------------------------------------------------------------
@@ -62,7 +62,7 @@ toDecimalChars : ℕ → List Char
 toDecimalChars = List.map toDigitChar ∘′ toNatDigits 10
 
 show : ℕ → String
-show = String.fromList ∘ toDecimalChars
+show = String.fromList ∘′ toDecimalChars
 
 -- Arbitrary base betwen 2 & 16.
 -- Warning: when compiled the time complexity of `showInBase b n` is

src/Data/Product.agda

@@ -23,18 +23,11 @@ private
 open import Data.Product.Base public
 
 ------------------------------------------------------------------------
--- Existential quantifiers
-
-∃ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
-∃ = Σ _
+-- Negation of existential quantifier
 
 ∄ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
 ∄ P = ¬ ∃ P
 
-∃₂ : ∀ {A : Set a} {B : A → Set b}
-     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
-∃₂ C = ∃ λ a → ∃ λ b → C a b
-
 -- Unique existence (parametrised by an underlying equality).
 
 ∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)

src/Data/Product/Base.agda

@@ -41,6 +41,16 @@ infix 2 Σ-syntax
 
 syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
 
+------------------------------------------------------------------------
+-- Existential quantifiers
+
+∃ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃ = Σ _
+
+∃₂ : ∀ {A : Set a} {B : A → Set b}
+     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
+∃₂ C = ∃ λ a → ∃ λ b → C a b
+
 ------------------------------------------------------------------------
 -- Definition of non-dependent products
 

src/Data/Product/Effectful/Left.agda

@@ -18,7 +18,7 @@ open import Level
 module Data.Product.Effectful.Left
   {a e} (A : RawMonoid a e) (b : Level) where
 
-open import Data.Product
+open import Data.Product.Base
 import Data.Product.Effectful.Left.Base as Base
 open import Effect.Applicative using (RawApplicative)
 open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)

src/Data/Product/Effectful/Left/Base.agda

@@ -17,7 +17,7 @@ open import Level
 module Data.Product.Effectful.Left.Base
   {a} (A : Set a) (b : Level) where
 
-open import Data.Product using (_×_; map₂; proj₁; proj₂; <_,_>)
+open import Data.Product.Base using (_×_; map₂; proj₁; proj₂; <_,_>)
 open import Effect.Functor using (RawFunctor)
 open import Effect.Comonad using (RawComonad)
 

src/Data/Product/Effectful/Right.agda

@@ -18,7 +18,7 @@ open import Level
 module Data.Product.Effectful.Right
   (a : Level) {b e} (B : RawMonoid b e) where
 
-open import Data.Product
+open import Data.Product.Base
 import Data.Product.Effectful.Right.Base as Base
 open import Effect.Applicative using (RawApplicative)
 open import Effect.Monad using (RawMonad; RawMonadT; mkRawMonad)

src/Data/Product/Effectful/Right/Base.agda

@@ -17,7 +17,7 @@ open import Level
 module Data.Product.Effectful.Right.Base
   {b} (B : Set b) (a : Level) where
 
-open import Data.Product using (_×_; map₁; proj₁; proj₂; <_,_>)
+open import Data.Product.Base using (_×_; map₁; proj₁; proj₂; <_,_>)
 open import Effect.Functor using (RawFunctor)
 open import Effect.Comonad using (RawComonad)
 

src/Data/String/Base.agda

@@ -8,7 +8,6 @@
 
 module Data.String.Base where
 
-open import Level using (zero)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Char.Base as Char using (Char)
 open import Data.List.Base as List using (List; [_]; _∷_; [])
@@ -17,13 +16,13 @@ open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
 open import Data.List.Relation.Binary.Lex.Core using (Lex-<; Lex-≤)
 open import Data.Maybe.Base as Maybe using (Maybe)
 open import Data.Nat.Base using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉)
-open import Data.Product using (proj₁; proj₂)
+open import Data.Product.Base using (proj₁; proj₂)
 open import Function.Base using (_on_; _∘′_; _∘_)
-open import Level using (Level)
+open import Level using (Level; 0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 
 ------------------------------------------------------------------------
 -- From Agda.Builtin: type and renamed primitives
@@ -47,17 +46,17 @@ open String public using ( String )
 -- Pointwise equality on Strings
 
 infix 4 _≈_
-_≈_ : Rel String zero
+_≈_ : Rel String 0ℓ
 _≈_ = Pointwise _≡_ on toList
 
 -- Lexicographic ordering on Strings
 
 infix 4 _<_
-_<_ : Rel String zero
+_<_ : Rel String 0ℓ
 _<_ = Lex-< _≡_ Char._<_ on toList
 
 infix 4 _≤_
-_≤_ : Rel String zero
+_≤_ : Rel String 0ℓ
 _≤_ = Lex-≤ _≡_ Char._<_ on toList
 
 ------------------------------------------------------------------------

src/Data/String/Unsafe.agda

@@ -12,7 +12,7 @@ import Data.List.Base as List
 import Data.List.Properties as Listₚ
 open import Data.Maybe.Base using (maybe′)
 open import Data.Nat.Base using (zero; suc; _+_)
-open import Data.Product using (proj₂)
+open import Data.Product.Base using (proj₂)
 open import Data.String.Base
 open import Function.Base using (_∘′_)
 

src/Data/Vec/Base.agda

@@ -12,12 +12,12 @@ open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
-open import Data.Product as Prod using (∃; ∃₂; _×_; _,_)
+open import Data.Product.Base as Prod using (∃; ∃₂; _×_; _,_)
 open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (const; _∘′_; id; _∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 open import Relation.Unary using (Pred; Decidable)
 
 private

src/Data/Vec/Bounded/Base.agda

@@ -8,21 +8,20 @@
 
 module Data.Vec.Bounded.Base where
 
-open import Level using (Level)
 open import Data.Nat.Base
 import Data.Nat.Properties as ℕₚ
 open import Data.List.Base as List using (List)
 open import Data.List.Extrema ℕₚ.≤-totalOrder
 open import Data.List.Relation.Unary.All as All using (All)
 import Data.List.Relation.Unary.All.Properties as Allₚ
 open import Data.List.Membership.Propositional using (mapWith∈)
-open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
+open import Data.Product.Base using (∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.These.Base as These using (These)
-open import Function
-open import Relation.Nullary
-open import Relation.Unary
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Function.Base using (_∘_; id; _$_)
+open import Level using (Level)
+open import Relation.Nullary.Decidable.Core using (recompute)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 
 private
   variable

src/Data/Vec/Functional.agda

@@ -18,10 +18,10 @@ module Data.Vec.Functional where
 open import Data.Fin.Base
 open import Data.List.Base as L using (List)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred)
-open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
+open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Base as V using (Vec)
-open import Function.Base
+open import Function.Base using (_∘_; const; flip; _ˢ_; id)
 open import Level using (Level)
 
 infixr 5 _∷_ _++_