Simplify Data.Sum and leftover Data.List imports

README/Case.agda

@@ -12,8 +12,6 @@ module README.Case where
 open import Data.Fin   hiding (pred)
 open import Data.Maybe hiding (from-just)
 open import Data.Nat   hiding (pred)
-open import Data.List
-open import Data.Sum
 open import Data.Product
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary

README/Data/Container/FreeMonad.agda

@@ -15,7 +15,7 @@ open import Data.Empty
 open import Data.Unit
 open import Data.Bool.Base using (Bool; true)
 open import Data.Nat
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base renaming (_×_ to _⟨×⟩_)
 open import Data.Container using (Container; _▷_)
 open import Data.Container.Combinator

README/Design/Decidability.agda

@@ -9,7 +9,7 @@
 module README.Design.Decidability where
 
 open import Data.Bool
-open import Data.List
+open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Properties using (∷-injective)
 open import Data.Nat
 open import Data.Nat.Properties using (suc-injective)

README/Design/Hierarchies.agda

@@ -8,7 +8,7 @@
 
 module README.Design.Hierarchies where
 
-open import Data.Sum using (_⊎_)
+open import Data.Sum.Base using (_⊎_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary using (_Preserves₂_⟶_⟶_)
 

README/Nary.agda

@@ -16,7 +16,7 @@ open import Data.Fin using (Fin; fromℕ; #_; inject₁)
 open import Data.List
 open import Data.List.Properties
 open import Data.Product using (_×_; _,_)
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Function
 open import Relation.Nullary
 open import Relation.Binary using (module Tri); open Tri

src/Algebra/Construct/Flip/Op.agda

@@ -11,7 +11,7 @@ module Algebra.Construct.Flip.Op where
 
 open import Algebra
 import Data.Product.Base as Prod
-import Data.Sum as Sum
+import Data.Sum.Base as Sum
 open import Function.Base using (flip)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)

src/Algebra/Construct/NaturalChoice/Min.agda

@@ -9,7 +9,7 @@
 open import Algebra.Core
 open import Algebra.Bundles
 open import Algebra.Construct.NaturalChoice.Base
-open import Data.Sum using (inj₁; inj₂; [_,_])
+open import Data.Sum.Base using (inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 open import Relation.Binary

src/Algebra/Construct/Subst/Equality.agda

@@ -19,7 +19,7 @@ module Algebra.Construct.Subst.Equality
 
 open import Algebra.Definitions
 open import Algebra.Structures
-import Data.Sum as Sum
+import Data.Sum.Base as Sum
 open import Function.Base
 open import Relation.Binary.Construct.Subst.Equality equiv
 

src/Algebra/Lattice/Construct/Subst/Equality.agda

@@ -12,7 +12,6 @@
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
 open import Algebra.Lattice.Structures
-import Data.Sum as Sum
 open import Data.Product as Prod
 open import Function.Base
 open import Relation.Binary.Core

src/Algebra/Module/Definitions/Left.agda

@@ -15,7 +15,6 @@ module Algebra.Module.Definitions.Left
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-open import Data.Sum
 open import Data.Product
 
 ------------------------------------------------------------------------

src/Algebra/Module/Definitions/Right.agda

@@ -16,7 +16,6 @@ module Algebra.Module.Definitions.Right
   where
 
 open import Data.Product
-open import Data.Sum
 
 ------------------------------------------------------------------------
 -- Binary operations

src/Data/Container/Indexed/Combinator.agda

@@ -13,7 +13,7 @@ open import Data.Container.Indexed
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product as Prod hiding (Σ) renaming (_×_ to _⟨×⟩_)
-open import Data.Sum renaming (_⊎_ to _⟨⊎⟩_)
+open import Data.Sum.Base renaming (_⊎_ to _⟨⊎⟩_)
 open import Data.Sum.Relation.Unary.All as All using (All)
 open import Function.Base as F hiding (id; const) renaming (_∘_ to _⟨∘⟩_)
 open import Function.Inverse using (_↔̇_; inverse)

src/Data/List/Relation/Unary/Enumerates/Setoid.agda

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
+open import Data.List.Base using (List)
 open import Level
 open import Relation.Binary
 

src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda

@@ -11,7 +11,7 @@ open import Data.List.Membership.Setoid.Properties as Membership
 open import Data.List.Relation.Unary.Any using (index)
 open import Data.List.Relation.Unary.Any.Properties using (lookup-index)
 open import Data.List.Relation.Unary.Enumerates.Setoid
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Sum.Relation.Binary.Pointwise
   using (_⊎ₛ_; inj₁; inj₂)
 open import Data.Product using (_,_; proj₁; proj₂)

src/Data/List/Relation/Unary/First.agda

@@ -16,7 +16,7 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product as Prod using (∃; -,_; _,_)
-open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function
 open import Relation.Unary
 open import Relation.Nullary

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

@@ -10,7 +10,7 @@ module Data.List.Relation.Unary.Grouped where
 
 open import Data.List.Base using (List; []; _∷_; map)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_; all?)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; _,_)
 open import Relation.Binary as B using (REL; Rel)
 open import Relation.Unary as U using (Pred)

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

@@ -9,7 +9,7 @@
 module Data.List.Relation.Unary.Grouped.Properties where
 
 open import Data.Bool using (true; false)
-open import Data.List
+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; []; _∷_)

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

@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
+open import Data.List.Base using ([]; _∷_; deduplicate)
 import Data.List.Relation.Unary.Unique.DecSetoid as Unique
 open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.Setoid.Properties

src/Data/Nat/Binary/Subtraction.agda

@@ -17,7 +17,7 @@ open import Data.Nat.Binary.Base
 open import Data.Nat.Binary.Properties
 import Data.Nat.Properties as ℕₚ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Vec using ([]; _∷_)
 open import Function.Base using (_∘_; _$_)
 open import Level using (0ℓ)

src/Data/Nat/Combinatorics/Specification.agda

@@ -16,7 +16,7 @@ open import Data.Nat.DivMod
 open import Data.Nat.Divisibility
 open import Data.Nat.Properties
 open import Data.Nat.Combinatorics.Base
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; trans; _≢_)
 open import Relation.Nullary.Decidable using (yes; no; does)

src/Data/Nat/InfinitelyOften.agda

@@ -14,7 +14,7 @@ open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product as Prod hiding (map)
-open import Data.Sum hiding (map)
+open import Data.Sum.Base using (inj₁; inj₂; _⊎_)
 open import Function
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Negation using (¬_)

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda

@@ -17,7 +17,7 @@ open import Data.Maybe.Properties using (just-injective)
 open import Data.Maybe.Relation.Unary.All as Maybe using (nothing; just)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product as Prod using (∃; ∃-syntax; _×_; _,_; proj₁; proj₂)
-open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base as F
 open import Level using (Level)
 

src/Data/Tree/AVL/Map/Membership/Propositional.agda

@@ -17,7 +17,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Maybe.Base using (just; nothing; is-just)
 open import Data.Product as Prod using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
 

src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda

@@ -17,7 +17,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Maybe.Base using (just; nothing; is-just)
 open import Data.Product as Prod using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
 

src/Data/Vec/Relation/Binary/Lex/Core.agda

@@ -12,7 +12,7 @@ open import Data.Empty
 open import Data.Nat using (ℕ; suc)
 import Data.Nat.Properties as ℕ
 open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
-open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
 open import Function.Base using (flip)

src/Effect/Monad/Error/Transformer.agda

@@ -41,7 +41,7 @@ record RawMonadError
 
 module Sumₗ where
 
-  open import Data.Sum using (inj₁; inj₂; [_,_]′)
+  open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
   open import Data.Sum.Effectful.Left.Transformer E a
 
   monadError : RawMonad M → RawMonadError (SumₗT M)
@@ -54,7 +54,7 @@ module Sumₗ where
 
 module Sumᵣ where
 
-  open import Data.Sum using (inj₁; inj₂; [_,_]′)
+  open import Data.Sum.Base using (inj₁; inj₂; [_,_]′)
   open import Data.Sum.Effectful.Right.Transformer a E
 
   monadError : RawMonad M → RawMonadError (SumᵣT M)

src/Reflection/External.agda

@@ -14,7 +14,7 @@ open import Data.Nat.Base using (ℕ; suc; zero; NonZero)
 open import Data.List.Base using (List; _∷_; [])
 open import Data.Product using (_×_; _,_)
 open import Data.String.Base as String using (String; _++_)
-open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Unit.Base using (⊤; tt)
 open import Function.Base using (case_of_; _$_; _∘_)
 open import Reflection hiding (name)

src/Relation/Nullary/Universe.agda

@@ -16,7 +16,7 @@ open import Relation.Binary.PropositionalEquality as PropEq
   using (_≡_; refl)
 import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
   as Trivial
-open import Data.Sum     as Sum  hiding (map)
+open import Data.Sum.Base as Sum  hiding (map)
 open import Data.Sum.Relation.Binary.Pointwise
 open import Data.Product as Prod hiding (map)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent

src/Relation/Unary/Algebra.agda

@@ -15,7 +15,7 @@ import Algebra.Lattice.Structures as AlgebraicLatticeStructures
 import Algebra.Structures as AlgebraicStructures
 open import Data.Empty.Polymorphic using (⊥-elim)
 open import Data.Product as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
-open import Data.Sum as Sum using (inj₁; inj₂; [_,_])
+open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
 open import Data.Unit.Polymorphic using (tt)
 open import Function.Base using (id; const; _∘_)
 open import Level