Tighten imports some more

doc/README/Effect/Monad/Partiality.agda

@@ -0,0 +1,27 @@
+-----------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example showing the use of the partiality Monad
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe --guardedness #-}
+
+module README.Effect.Monad.Partiality where
+
+open import Codata.Musical.Notation using (♯_)
+open import Data.Bool.Base using (false; true)
+open import Data.Nat using (ℕ; _+_; _∸_; _≤?_)
+open import Effect.Monad.Partiality
+open import Relation.Nullary.Decidable using (does)
+
+open Workaround
+
+-- McCarthy's f91:
+
+f91′ : ℕ → ℕ ⊥P
+f91′ n with does (n ≤? 100)
+... | true  = later (♯ (f91′ (11 + n) >>= f91′))
+... | false = now (n ∸ 10)
+
+f91 : ℕ → ℕ ⊥
+f91 n = ⟦ f91′ n ⟧P

src/Algebra/Module/Construct/Idealization.agda

@@ -43,9 +43,11 @@ import Algebra.Definitions as Definitions
 import Algebra.Module.Construct.DirectProduct as DirectProduct
 import Algebra.Module.Construct.TensorUnit as TensorUnit
 open import Algebra.Structures using (IsAbelianGroup; IsRing)
-open import Data.Product using (_,_; ∃-syntax)
+open import Data.Product.Base using (_,_; ∃-syntax)
 open import Level using (Level; _⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Bundles using  (Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsEquivalence)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------

src/Algebra/Properties/CommutativeMonoid.agda

@@ -6,9 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles
-open import Algebra.Definitions
-open import Data.Product using (_,_; proj₂)
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Algebra.Definitions using (LeftInvertible; RightInvertible; Invertible)
+open import Data.Product.Base using (_,_; proj₂)
 
 module Algebra.Properties.CommutativeMonoid
   {g₁ g₂} (M : CommutativeMonoid g₁ g₂) where

src/Data/Container/Core.agda

@@ -8,10 +8,10 @@
 
 module Data.Container.Core where
 
-open import Level
+open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base as Product using (Σ-syntax)
-open import Function.Base
-open import Function using (Inverse; _↔_)
+open import Function.Base using (_∘_; _∘′_)
+open import Function.Bundles using (Inverse; _↔_)
 open import Relation.Unary using (Pred; _⊆_)
 
 -- Definition of Containers

src/Data/Container/Indexed.agda

@@ -11,14 +11,14 @@
 
 module Data.Container.Indexed where
 
-open import Level
+open import Level using (Level; zero; _⊔_)
 open import Data.Product.Base as Prod hiding (map)
-open import Data.W.Indexed
+open import Data.W.Indexed using (W)
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
-open import Function using (_↔_; Inverse)
+open import Function.Bundles using (_↔_; Inverse)
 open import Relation.Unary using (Pred; _⊆_)
 open import Relation.Binary.Core using (Rel; REL)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; trans; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≗_; refl; trans; subst)
 
 ------------------------------------------------------------------------
 

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

@@ -8,11 +8,11 @@
 
 module Data.Container.Indexed.Relation.Binary.Pointwise where
 
-open import Data.Product using (_,_; Σ-syntax)
-open import Function
+open import Data.Product.Base using (_,_; Σ-syntax)
+open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary using (REL; _⇒_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧)
 

src/Data/List/Properties.agda

@@ -23,7 +23,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base
-open import Data.Nat.Divisibility
+open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
 open import Data.Product.Base as Product
   using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)

src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda

@@ -13,10 +13,10 @@ module Data.List.Relation.Ternary.Appending.Setoid.Properties
   where
 
 open import Data.List.Base as List using (List; [])
-import Data.List.Properties as Listₚ
+import Data.List.Properties as List
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
 import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
-open import Data.Product using (∃-syntax; _×_; _,_)
+open import Data.Product.Base using (∃-syntax; _×_; _,_)
 open import Function.Base using (id)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
@@ -45,7 +45,7 @@ open Appendingₚ public
 ++[]⁻¹ : Appending as [] cs → Pointwise _≈_ as cs
 ++[]⁻¹ {as} {cs} ls with break ls
 ... | cs₁ , cs₂ , refl , pw , []
-  rewrite Listₚ.++-identityʳ cs₁
+  rewrite List.++-identityʳ cs₁
   = pw
 
 respʳ-≋ : ∀ {cs′} → Appending as bs cs → Pointwise _≈_ cs cs′ →

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

@@ -8,17 +8,16 @@
 
 module Data.List.Relation.Unary.First.Properties where
 
-open import Data.Empty
 open import Data.Fin.Base using (suc)
 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 (here; there)
 open import Data.List.Relation.Unary.First
 import Data.Sum as Sum
 open import Function.Base using (_∘′_; _$_; _∘_; id)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl; _≗_)
-open import Relation.Unary
-open import Relation.Nullary.Negation
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
+open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
+open import Relation.Nullary.Negation using (contradiction)
 
 ------------------------------------------------------------------------
 -- map
@@ -52,7 +51,7 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 
   All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
-  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = ⊥-elim (p⇒¬q px qx)
+  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = contradiction qx (p⇒¬q px)
   All⇒¬First p⇒¬q (_ ∷ pxs)  (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf
 
   First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
@@ -64,16 +63,16 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 
   unique-index : ∀ {xs} → P ⊆ ∁ Q → (f₁ f₂ : First P Q xs) → index f₁ ≡ index f₂
   unique-index p⇒¬q [ _ ]    [ _ ]    = refl
-  unique-index p⇒¬q [ qx ]   (px ∷ _) = ⊥-elim (p⇒¬q px qx)
-  unique-index p⇒¬q (px ∷ _) [ qx ]   = ⊥-elim (p⇒¬q px qx)
+  unique-index p⇒¬q [ qx ]   (px ∷ _) = contradiction qx (p⇒¬q px)
+  unique-index p⇒¬q (px ∷ _) [ qx ]   = contradiction qx (p⇒¬q px)
   unique-index p⇒¬q (_ ∷ f₁) (_ ∷ f₂) = ≡.cong suc (unique-index p⇒¬q f₁ f₂)
 
   irrelevant : P ⊆ ∁ Q → Irrelevant P → Irrelevant Q → Irrelevant (First P Q)
-  irrelevant p⇒¬q p-irr q-irr [ qx₁ ]    [ qx₂ ]    = ≡.cong [_] (q-irr qx₁ qx₂)
-  irrelevant p⇒¬q p-irr q-irr [ qx₁ ]    (px₂ ∷ f₂) = ⊥-elim (p⇒¬q px₂ qx₁)
-  irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) [ qx₂ ]    = ⊥-elim (p⇒¬q px₁ qx₂)
-  irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) (px₂ ∷ f₂) =
-    ≡.cong₂ _∷_ (p-irr px₁ px₂) (irrelevant p⇒¬q p-irr q-irr f₁ f₂)
+  irrelevant p⇒¬q p-irr q-irr [ px ]    [ qx ]    = ≡.cong [_] (q-irr px qx)
+  irrelevant p⇒¬q p-irr q-irr [ qx ]    (px ∷ _)  = contradiction qx (p⇒¬q px)
+  irrelevant p⇒¬q p-irr q-irr (px ∷ _)  [ qx ]    = contradiction qx (p⇒¬q px)
+  irrelevant p⇒¬q p-irr q-irr (px ∷ f)  (qx ∷ g) =
+    ≡.cong₂ _∷_ (p-irr px qx) (irrelevant p⇒¬q p-irr q-irr f g)
 
 ------------------------------------------------------------------------
 -- Decidability

src/Data/Nat/Primality/Factorisation.agda

@@ -8,28 +8,33 @@
 
 module Data.Nat.Primality.Factorisation where
 
-open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
+  using (_∣?_; quotient; quotient>1; quotient-<; quotient-∣; m∣n⇒n≡m*quotient; _∣_; ∣1⇒≡1;
+        divides)
 open import Data.Nat.Properties
 open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
 open import Data.Nat.Primality
-open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂)
+  using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
+         2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
+open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
 open import Data.List.Base using (List; []; _∷_; _++_; product)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties using (∈-∃++)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Binary.Permutation.Propositional
   using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift)
+open import Data.List.Relation.Binary.Permutation.Propositional.Properties
+  using (product-↭; All-resp-↭; shift)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_; _|>_; flip)
 open import Induction using (build)
 open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
 
 private
   variable

src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda

@@ -9,13 +9,16 @@
 module Data.Product.Relation.Binary.Pointwise.NonDependent where
 
 open import Data.Product.Base as Product
-open import Data.Product.Properties using (≡-dec)
-open import Data.Sum.Base
-open import Data.Unit.Base using (⊤)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level; _⊔_; 0ℓ)
-open import Function
+open import Function.Base using (_on_; id)
+open import Function.Bundles using (Inverse)
 open import Relation.Nullary.Decidable using (_×-dec_)
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Bundles
+  using (Setoid; DecSetoid; Preorder; Poset; StrictPartialOrder)
+open import Relation.Binary.Definitions
+open import Relation.Binary.Structures
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 

src/Data/Rational/Unnormalised/Base.agda

@@ -9,6 +9,7 @@
 module Data.Rational.Unnormalised.Base where
 
 open import Algebra.Bundles.Raw
+  using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Integer.Base as ℤ
   using (ℤ; +_; +0; +[1+_]; -[1+_]; +<+; +≤+)

src/Data/Sum/Algebra.agda

@@ -8,12 +8,16 @@
 
 module Data.Sum.Algebra where
 
-open import Algebra
+open import Algebra.Bundles
+  using (Magma; Semigroup; Monoid; CommutativeMonoid)
+open import Algebra.Definitions
+open import Algebra.Structures
+  using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid)
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_,_)
-open import Data.Sum.Base
-open import Data.Sum.Properties
-open import Data.Unit.Polymorphic using (⊤; tt)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; map; [_,_]; swap; assocʳ; assocˡ)
+open import Data.Sum.Properties using (swap-involutive)
+open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Function.Base using (id; _∘_)
 open import Function.Properties.Inverse using (↔-isEquivalence)
 open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′)

src/Data/Sum/Function/Propositional.agda

@@ -8,15 +8,18 @@
 
 module Data.Sum.Function.Propositional where
 
-open import Data.Sum.Base
+open import Data.Sum.Base using (_⊎_)
 open import Data.Sum.Function.Setoid
 open import Data.Sum.Relation.Binary.Pointwise using (Pointwise-≡↔≡; _⊎ₛ_)
 open import Function.Construct.Composition as Compose
 open import Function.Related.Propositional
-open import Function
+open import Function.Base using (id)
+open import Function.Bundles
+  using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _↩_; _↪_; _⤖_; _↔_)
 open import Function.Properties.Inverse as Inv
 open import Level using (Level; _⊔_)
-open import Relation.Binary using (REL; Setoid)
+open import Relation.Binary.Core using (REL)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality using (setoid)
 
 private

src/Data/Unit/Polymorphic/Properties.agda

@@ -23,6 +23,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Decidable; Antisymmetric; Total)
 open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; trans; decSetoid; setoid; isEquivalence)
 
 private
   variable

src/Effect/Monad/Partiality.agda

@@ -8,15 +8,15 @@
 
 module Effect.Monad.Partiality where
 
-open import Codata.Musical.Notation
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
+open import Codata.Musical.Notation using (∞; ♯_; ♭)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; module Join)
 open import Data.Bool.Base using (Bool; false; true)
-open import Data.Nat using (ℕ; zero; suc; _+_)
-open import Data.Product as Prod hiding (map)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Product as Prod using (∃; ∄; -,_; ∃₂; _,_; _×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function.Base
+open import Function.Base using (_∘′_; flip; id; _∘_; _$_; _⟨_⟩_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core as B hiding (Rel; _⇔_)
@@ -29,9 +29,8 @@ open import Relation.Binary.Bundles
 import Relation.Binary.Properties.Setoid as SetoidProperties
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Relation.Nullary
-open import Relation.Nullary.Decidable hiding (map)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Decidable using (yes; no; False; Dec; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation using (¬_; ¬¬-Monad)
 
 private
   variable
@@ -934,22 +933,3 @@ idempotent {A = A} B x f = sound (idem x)
                                                      laterˡ (refl (Setoid.refl B))) ⟩
     (♭ x >>= λ y′ →     ♭ x >>= λ y″ → f y′ y″)  ≳⟨ idem (♭ x) ⟩≅
     (♭ x >>= λ y′ → f y′ y′)                     ∎))
-
-------------------------------------------------------------------------
--- Example
-
-private
- module Example where
-
-  open Data.Nat
-  open Workaround
-
-  -- McCarthy's f91:
-
-  f91′ : ℕ → ℕ ⊥P
-  f91′ n with does (n ≤? 100)
-  ... | true  = later (♯ (f91′ (11 + n) >>= f91′))
-  ... | false = now (n ∸ 10)
-
-  f91 : ℕ → ℕ ⊥
-  f91 n = ⟦ f91′ n ⟧P

src/Function/Properties/Inverse/HalfAdjointEquivalence.agda

@@ -8,10 +8,12 @@
 
 module Function.Properties.Inverse.HalfAdjointEquivalence where
 
-open import Function.Base
-open import Function
-open import Level
+open import Function.Base using (id; _∘_)
+open import Function.Bundles using (Inverse; _↔_; mk↔ₛ′)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; cong; sym; trans; trans-reflʳ; cong-≡id; cong-∘; naturality;
+         cong-id; trans-assoc; trans-symˡ; module ≡-Reasoning)
 
 private
   variable