[imports] Data.List.Effectful.* .. Relation.Nullary

src/Data/List/Effectful/Foldable.agda

@@ -15,7 +15,7 @@ open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Effect.Foldable using (RawFoldableWithDefaults; RawFoldable)
 open import Function.Base using (_∘_; id)
 open import Level using (Level)
-import Relation.Binary.PropositionalEquality.Core as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; cong)
 
 private
   variable

src/Data/List/Effectful/Transformer.agda

@@ -9,13 +9,12 @@
 module Data.List.Effectful.Transformer where
 
 open import Data.List.Base as List using (List; []; _∷_)
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
-open import Function.Base
-open import Level
-
 import Data.List.Effectful as List
+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)
 
 private
   variable

src/Data/List/Extrema/Core.agda

@@ -6,22 +6,25 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Definitions using (Trans)
 open import Relation.Binary.Bundles using (TotalOrder; Setoid)
 
 module Data.List.Extrema.Core
   {b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where
 
-open import Algebra.Core
-open import Algebra.Definitions
+open import Algebra.Construct.LiftedChoice
+  using (Lift; sel-≡; preservesᵒ; preservesᵇ ; forcesᵇ)
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions using (Selective)
 import Algebra.Construct.NaturalChoice.Min as Min
+  using (_⊓_; x⊓y≈y⇒y≤x; x⊓y≈x⇒x≤y; ⊓-sel; ⊓-isSelectiveMagma)
 import Algebra.Construct.NaturalChoice.Max as Max
+  using (_⊔_; x⊔y≈y⇒x≤y; x⊔y≈x⇒y≤x; ⊔-sel; ⊔-isSelectiveMagma)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.Definitions using (Trans)
 
-open import Algebra.Construct.LiftedChoice
 
 open TotalOrder totalOrder renaming (Carrier to B)
 open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_

src/Data/List/Fresh.agda

@@ -26,7 +26,7 @@ open import Relation.Nullary using (does)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core using (Rel)
 import Relation.Binary.Definitions as B
-open import Relation.Nary
+open import Relation.Nary using (∀[_]; _⇒_)
 
 private
   variable

src/Data/List/Fresh/Membership/Setoid.agda

@@ -6,15 +6,15 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Fresh.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Level using (Level; _⊔_)
-open import Data.List.Fresh
+open import Data.List.Fresh using (List#)
 open import Data.List.Fresh.Relation.Unary.Any as Any using (Any)
-open import Relation.Nullary
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 open Setoid S renaming (Carrier to A)
 

src/Data/List/Fresh/Membership/Setoid/Properties.agda

@@ -6,30 +6,32 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
 
-module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ) where
+module Data.List.Fresh.Membership.Setoid.Properties {c ℓ} (S : Setoid c ℓ)
+  where
 
 open import Level using (Level; _⊔_)
-open import Data.Empty
-open import Data.Nat.Base
-open import Data.Nat.Properties
+open import Data.List.Fresh
+open import Data.List.Fresh.Properties using (fresh-respectsˡ)
+open import Data.List.Fresh.Membership.Setoid S using (_∈_; _∉_)
+open import Data.List.Fresh.Relation.Unary.Any using (Any; here; there; _─_)
+import Data.List.Fresh.Relation.Unary.Any.Properties as List#
+  using (length-remove)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat.Base using (ℕ; suc; zero; _≤_; _<_; z≤n; s≤s; z<s; s<s)
+open import Data.Nat.Properties using (module ≤-Reasoning)
 open import Data.Product.Base using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂)
-
 open import Function.Base using (id; _∘′_; _$_)
-open import Relation.Nullary
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary using (Irrelevant)
 open import Relation.Unary as Unary using (Pred)
-import Relation.Binary.Definitions as Binary
+import Relation.Binary.Definitions as Binary using (_Respectsˡ_; Irrelevant)
 import Relation.Binary.PropositionalEquality.Core as ≡
-open import Relation.Nary
-
-open import Data.List.Fresh
-open import Data.List.Fresh.Properties
-open import Data.List.Fresh.Membership.Setoid S
-open import Data.List.Fresh.Relation.Unary.Any using (Any; here; there; _─_)
-import Data.List.Fresh.Relation.Unary.Any.Properties as List#
+  using (_≡_; cong; sym; subst)
+open import Relation.Nary using (∀[_]; _⇒_)
 
 open Setoid S renaming (Carrier to A)
 

src/Data/List/Fresh/NonEmpty.agda

@@ -8,11 +8,11 @@
 
 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.Base using (ℕ; suc)
 open import Data.Product.Base using (_×_; _,_)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
 
 private

src/Data/List/Fresh/Properties.agda

@@ -8,14 +8,15 @@
 
 module Data.List.Fresh.Properties where
 
-open import Level using (Level; _⊔_)
+open import Data.List.Fresh using (List#; _∷#_; _#_; Empty; NonEmpty; cons; [])
 open import Data.Product.Base using (_,_)
-open import Relation.Nullary
+open import Level using (Level; _⊔_)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Unary as U using (Pred)
-import Relation.Binary.Definitions as B
+import Relation.Binary.Definitions as B using (_Respectsˡ_; Irrelevant)
 open import Relation.Binary.Core using (Rel)
 
-open import Data.List.Fresh
 
 private
   variable

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

@@ -8,16 +8,17 @@
 
 module Data.List.Fresh.Relation.Unary.All where
 
-open import Level using (Level; _⊔_; Lift)
+open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
+open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product.Base using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘_; _$_)
+open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
-open import Relation.Unary  as U
+open import Relation.Unary as U
+  using (Pred; IUniversal; Universal; Decidable; _⇒_; _∪_; _∩_)
 open import Relation.Binary.Core using (Rel)
 
-open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
-open import Data.List.Fresh.Relation.Unary.Any as Any using (Any; here; there)
 
 private
   variable

src/Data/List/Fresh/Relation/Unary/All/Properties.agda

@@ -8,18 +8,19 @@
 
 module Data.List.Fresh.Relation.Unary.All.Properties where
 
-open import Level using (Level; _⊔_; Lift)
-open import Data.Empty
+open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
+open import Data.List.Fresh.Relation.Unary.All using (All; []; _∷_; append)
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘′_)
-open import Relation.Nullary
-open import Relation.Unary  as U
+open import Level using (Level; _⊔_; Lift)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Unary  as U using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
-open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
-open import Data.List.Fresh.Relation.Unary.All
+
 
 private
   variable

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

@@ -9,16 +9,16 @@
 module Data.List.Fresh.Relation.Unary.Any where
 
 open import Level using (Level; _⊔_; Lift)
+open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
 open import Data.Product.Base using (∃; _,_; -,_)
 open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Function.Bundles using (_⇔_; mk⇔)
+open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Nullary.Decidable as Dec using (Dec; no; _⊎-dec_)
-open import Relation.Unary  as U
+open import Relation.Unary  as U using (Pred; IUniversal; Universal; Decidable; _⇒_; _∪_; _∩_)
 open import Relation.Binary.Core using (Rel)
 
-open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
-
 private
   variable
     a p q r : Level

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

@@ -8,24 +8,24 @@
 
 module Data.List.Fresh.Relation.Unary.Any.Properties where
 
-open import Level using (Level; _⊔_; Lift)
 open import Data.Bool.Base using (true; false)
-open import Data.Empty
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.List.Fresh using (List#; _∷#_; _#_; NonEmpty; cons; length; [])
+open import Data.List.Fresh.Relation.Unary.All using (All; _∷_; append; [])
+open import Data.List.Fresh.Relation.Unary.Any using (Any; here; there; _─_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘′_)
+open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core
 open import Relation.Unary  as U using (Pred)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nary
+open import Relation.Nary using (∀[_]; _⇒_; ∁; Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
-open import Data.List.Fresh
-open import Data.List.Fresh.Relation.Unary.All
-open import Data.List.Fresh.Relation.Unary.Any
-
 private
   variable
     a b p q r s : Level

src/Data/List/Kleene/AsList.agda

@@ -18,7 +18,7 @@ private
     B : Set b
     C : Set c
 
-import Data.List.Kleene.Base as Kleene
+import Data.List.Kleene.Base as Kleene using ([])
 
 ------------------------------------------------------------------------
 -- Here we import half of the functions from Data.KleeneList: the half

src/Data/List/Kleene/Base.agda

@@ -8,15 +8,15 @@
 
 module Data.List.Kleene.Base where
 
+open import Algebra.Core using (Op₂)
 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; maybe′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
+open import Function.Base using (id; _$_; _∘_)
 open import Level using (Level)
 
-open import Algebra.Core using (Op₂)
-open import Function.Base
 
 private
   variable

src/Relation/Nary.agda

@@ -15,18 +15,20 @@ module Relation.Nary where
 ------------------------------------------------------------------------
 
 open import Level using (Level; _⊔_; Lift)
-open import Data.Unit.Base
+open import Data.Unit.Base using (⊤)
 open import Data.Bool.Base using (true; false)
-open import Data.Empty
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (zero; suc)
 open import Data.Product.Base as Product using (_×_; _,_)
 open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_$_; _∘′_)
 open import Function.Nary.NonDependent
 open import Relation.Nullary.Negation using (¬_)
-open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _because_; _×-dec_)
+open import Relation.Nullary.Decidable.Core as Dec
+  using (Dec; yes; no; _because_; _×-dec_)
 import Relation.Unary as Unary
+  using (Pred; Satisfiable; Universal; IUniversal)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 
 private