Simplify leftover Function imports (#2012)

* Simplify leftover `Function` imports

* `Function` -> `Function.Base`

Co-authored-by: G. Allais <[email protected]>

---------

Co-authored-by: G. Allais <[email protected]>

Author: Saransh-cpp

README/Data/Container/Indexed.agda

@@ -12,7 +12,7 @@ open import Data.Unit
 open import Data.Empty
 open import Data.Nat.Base
 open import Data.Product
-open import Function
+open import Function.Base using (_∋_)
 open import Data.W.Indexed
 open import Data.Container.Indexed
 open import Data.Container.Indexed.WithK

README/Design/Decidability.agda

@@ -15,7 +15,7 @@ open import Data.Nat
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Product
 open import Data.Unit
-open import Function
+open import Function.Base using (id;  _∘_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nary
 

README/Function/Reasoning.agda

@@ -36,7 +36,7 @@ open import Data.Nat
 open import Data.List.Base
 open import Data.Char.Base
 open import Data.String as String using (String; toList; fromList; _==_)
-open import Function
+open import Function.Base using (_∘_)
 open import Data.Bool hiding (_≤?_)
 open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)
 open import Agda.Builtin.Equality

README/Nary.agda

@@ -17,7 +17,7 @@ open import Data.List
 open import Data.List.Properties
 open import Data.Product using (_×_; _,_)
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Function
+open import Function.Base using (id; flip; _∘′_)
 open import Relation.Nullary
 open import Relation.Binary using (module Tri); open Tri
 open import Relation.Binary.PropositionalEquality

README/Tactic/RingSolver.agda

@@ -29,7 +29,6 @@ instance
 -- Imports!
 
 open import Data.List.Base as List using (List; _∷_; [])
-open import Function
 open import Relation.Binary.PropositionalEquality
   using (subst; cong; _≡_; module ≡-Reasoning)
 open import Data.Bool as Bool using (Bool; true; false; if_then_else_)

src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda

@@ -25,7 +25,7 @@ import Function.Identity.Effectful as IdCat
 open import Data.Vec.Properties using (lookup-map)
 open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
   using (Pointwise; ext)
-open import Function
+open import Function.Base using (_∘_; _$_; flip)
 open import Relation.Binary.PropositionalEquality as P using (_≗_)
 import Relation.Binary.Reflection as Reflection
 

src/Algebra/Properties/AbelianGroup.agda

@@ -12,7 +12,7 @@ module Algebra.Properties.AbelianGroup
   {a ℓ} (G : AbelianGroup a ℓ) where
 
 open AbelianGroup G
-open import Function
+open import Function.Base using (_$_)
 open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------

src/Algebra/Solver/Ring.agda

@@ -49,7 +49,7 @@ open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Vec.Base using (Vec; []; _∷_; lookup)
 open import Data.Maybe.Base using (just; nothing)
-open import Function
+open import Function.Base using (_⟨_⟩_; _$_)
 open import Level using (_⊔_)
 
 infix  9 :-_ -H_ -N_

src/Algebra/Solver/Ring/Lemmas.agda

@@ -24,7 +24,7 @@ open AlmostCommutativeRing r
 open import Algebra.Morphism
 open _-Raw-AlmostCommutative⟶_ morphism
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Function
+open import Function.Base using (_⟨_⟩_; _$_)
 
 lemma₀ : ∀ a b c x →
          (a + b) * x + c ≈ a * x + (b * x + c)

src/Axiom/Extensionality/Heterogeneous.agda

@@ -9,7 +9,7 @@
 module Axiom.Extensionality.Heterogeneous where
 
 import Axiom.Extensionality.Propositional as P
-open import Function
+open import Function.Base using (_$_; _∘_)
 open import Level
 open import Relation.Binary.HeterogeneousEquality.Core
 open import Relation.Binary.PropositionalEquality.Core

src/Codata/Sized/Delay/Effectful.agda

@@ -9,7 +9,7 @@
 module Codata.Sized.Delay.Effectful where
 
 open import Codata.Sized.Delay
-open import Function
+open import Function.Base using (id)
 open import Effect.Choice
 open import Effect.Empty
 open import Effect.Functor

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

@@ -9,7 +9,7 @@
 module Data.Container.Relation.Binary.Pointwise where
 
 open import Data.Product using (_,_; Σ-syntax; -,_; proj₁; proj₂)
-open import Function
+open import Function.Base using (_∘_)
 open import Level using (_⊔_)
 open import Relation.Binary using (REL; _⇒_)
 open import Relation.Binary.PropositionalEquality.Core as P

src/Data/Container/Relation/Unary/Any.agda

@@ -11,7 +11,7 @@ module Data.Container.Relation.Unary.Any where
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred; _⊆_)
 open import Data.Product as Prod using (_,_; proj₂; ∃)
-open import Function
+open import Function.Base using (_∘′_; id)
 
 open import Data.Container.Core hiding (map)
 import Data.Container.Morphism as M

src/Data/DifferenceList.agda

@@ -10,7 +10,7 @@ module Data.DifferenceList where
 
 open import Level using (Level)
 open import Data.List.Base as List using (List)
-open import Function
+open import Function.Base using (_⟨_⟩_)
 open import Data.Nat.Base
 
 private

src/Data/DifferenceNat.agda

@@ -10,7 +10,7 @@
 module Data.DifferenceNat where
 
 open import Data.Nat.Base as N using (ℕ)
-open import Function
+open import Function.Base using (_⟨_⟩_)
 
 infixl 6 _+_
 

src/Data/DifferenceVec.agda

@@ -10,7 +10,7 @@ module Data.DifferenceVec where
 
 open import Data.DifferenceNat
 open import Data.Vec.Base as V using (Vec)
-open import Function
+open import Function.Base using (_⟨_⟩_)
 import Data.Nat.Base as N
 
 infixr 5 _∷_ _++_

src/Data/Graph/Acyclic.agda

@@ -26,7 +26,7 @@ open import Data.Empty
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.List.Base as List using (List; []; _∷_)
-open import Function
+open import Function.Base using (_$_; _∘′_; _∘_; id)
 open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 

src/Data/Integer/Divisibility.agda

@@ -10,7 +10,7 @@
 
 module Data.Integer.Divisibility where
 
-open import Function
+open import Function.Base using (_on_; _$_)
 open import Data.Integer.Base
 open import Data.Integer.Properties
 import Data.Nat.Base as ℕ

src/Data/Integer/Divisibility/Signed.agda

@@ -8,7 +8,7 @@
 
 module Data.Integer.Divisibility.Signed where
 
-open import Function
+open import Function.Base using (_⟨_⟩_; _$_; _$′_; _∘_; _∘′_)
 open import Data.Integer.Base
 open import Data.Integer.Properties
 open import Data.Integer.Divisibility as Unsigned

src/Data/List/NonEmpty/Effectful.agda

@@ -16,7 +16,7 @@ open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad
 open import Effect.Comonad
-open import Function
+open import Function.Base using (flip; _∘′_; _∘_)
 
 ------------------------------------------------------------------------
 -- List⁺ applicative functor

src/Data/List/Properties.agda

@@ -31,7 +31,8 @@ import Data.Product.Relation.Unary.All as Prod using (All)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Fin.Properties using (toℕ-cast)
-open import Function
+open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
+open import Function.Definitions using (Injective)
 open import Level using (Level)
 open import Relation.Binary as B using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as EqR

src/Data/List/Relation/Ternary/Interleaving/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Nat.Properties using (+-suc)
 open import Data.List.Base hiding (_∷ʳ_)
 open import Data.List.Properties using (reverse-involutive)
 open import Data.List.Relation.Ternary.Interleaving hiding (map)
-open import Function
+open import Function.Base using (_$_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; module ≡-Reasoning)

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

@@ -16,7 +16,7 @@ open import Data.Bool.Base using (true; false)
 open import Relation.Unary using (Decidable)
 open import Relation.Nullary.Decidable using (does)
 open import Relation.Nullary.Decidable using (¬?)
-open import Function
+open import Function.Base using (_∘_)
 
 open import Data.List.Relation.Binary.Equality.Setoid S using (≋-refl)
 open import Data.List.Relation.Ternary.Interleaving.Setoid S

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

@@ -17,7 +17,9 @@ open import Data.Sum.Relation.Binary.Pointwise
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
   using (_×ₛ_)
-open import Function
+open import Function.Base using (_∘_)
+open import Function.Bundles using (Surjection)
+open import Function.Definitions using (Surjective)
 open import Level
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)

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

@@ -17,7 +17,7 @@ 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.Base as Sum using (_⊎_; inj₁; inj₂)
-open import Function
+open import Function.Base using (id; _∘′_)
 open import Relation.Unary
 open import Relation.Nullary
 

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

@@ -15,7 +15,7 @@ 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
+open import Function.Base using (_∘′_; _$_; _∘_; id)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; _≗_)
 open import Relation.Unary
 open import Relation.Nullary.Negation

src/Data/List/Reverse.agda

@@ -10,7 +10,7 @@ module Data.List.Reverse where
 
 open import Data.List.Base as L hiding (reverse)
 open import Data.List.Properties
-open import Function
+open import Function.Base using (_$_)
 open import Relation.Binary.PropositionalEquality
 
 -- If you want to traverse a list from the end, then you can use the

src/Data/List/Zipper.agda

@@ -11,7 +11,7 @@ module Data.List.Zipper where
 open import Data.Nat.Base
 open import Data.Maybe.Base as Maybe using (Maybe ; just ; nothing)
 open import Data.List.Base as List using (List ; [] ; _∷_)
-open import Function
+open import Function.Base using (_on_; flip)
 
 
 -- Definition

src/Data/List/Zipper/Properties.agda

@@ -15,7 +15,7 @@ open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
 open import Relation.Binary.PropositionalEquality
 open ≡-Reasoning
-open import Function
+open import Function.Base using (_on_; _$′_; _$_; flip)
 
 -- Invariant: Zipper represents a given list
 ------------------------------------------------------------------------

src/Data/Maybe/Properties.agda

@@ -14,7 +14,8 @@ import Algebra.Definitions as Definitions
 open import Data.Maybe.Base
 open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
 open import Data.Product using (_,_)
-open import Function
+open import Function.Base using (_∋_; id; _∘_; _∘′_)
+open import Function.Definitions using (Injective)
 open import Level using (Level)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality

src/Data/Maybe/Relation/Unary/All/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Maybe.Relation.Unary.All as All
   using (All; nothing; just)
 open import Data.Maybe.Relation.Binary.Connected
 open import Data.Product using (_×_; _,_)
-open import Function
+open import Function.Base using (_∘_)
 open import Level
 open import Relation.Unary
 open import Relation.Binary.Core

src/Data/Nat/Coprimality.agda

@@ -19,7 +19,7 @@ open import Data.Nat.Primality
 open import Data.Nat.Properties
 open import Data.Nat.DivMod
 open import Data.Product as Prod
-open import Function
+open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; refl; trans; cong; subst; module ≡-Reasoning)

src/Data/Nat/GCD.agda

@@ -17,7 +17,7 @@ open import Data.Nat.Induction
   using (Acc; acc; <′-Rec; <′-recBuilder; <-wellFounded-fast)
 open import Data.Product
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
-open import Function
+open import Function.Base using (_$_; _∘_)
 open import Induction using (build)
 open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Binary

src/Data/Nat/GCD/Lemmas.agda

@@ -11,7 +11,7 @@ module Data.Nat.GCD.Lemmas where
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Nat.Solver
-open import Function
+open import Function.Base using (_$_)
 open import Relation.Binary.PropositionalEquality
 
 open +-*-Solver

src/Data/Nat/InfinitelyOften.agda

@@ -15,7 +15,7 @@ open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product as Prod hiding (map)
 open import Data.Sum.Base using (inj₁; inj₂; _⊎_)
-open import Function
+open import Function.Base using (_∘_; id)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)

src/Data/Nat/LCM.agda

@@ -17,7 +17,6 @@ open import Data.Nat.Properties
 open import Data.Nat.GCD
 open import Data.Product
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
 open import Relation.Binary

src/Data/Product/Effectful/Examples.agda

@@ -16,7 +16,7 @@ open import Effect.Functor using (RawFunctor)
 open import Effect.Monad using (RawMonad)
 open import Data.Product
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-open import Function
+open import Function.Base using (id)
 import Function.Identity.Effectful as Id
 open import Relation.Binary using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

src/Data/Product/Properties/WithK.agda

@@ -9,7 +9,7 @@
 module Data.Product.Properties.WithK where
 
 open import Data.Product
-open import Function
+open import Function.Base using (_∋_)
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------

src/Data/Record.agda

@@ -14,7 +14,7 @@ open import Data.Empty
 open import Data.List.Base
 open import Data.Product hiding (proj₁; proj₂)
 open import Data.Unit.Polymorphic
-open import Function
+open import Function.Base using (id; _∘_)
 open import Level
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality

src/Data/Star/BoundedVec.agda

@@ -16,7 +16,7 @@ open import Data.Star.Decoration
 open import Data.Star.Pointer
 open import Data.Star.List using (List)
 open import Data.Unit
-open import Function
+open import Function.Base using (const)
 open import Relation.Binary
 open import Relation.Binary.Consequences
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive

src/Data/Star/Decoration.agda

@@ -9,7 +9,7 @@
 module Data.Star.Decoration where
 
 open import Data.Unit
-open import Function
+open import Function.Base using (flip)
 open import Level
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive

src/Data/Star/Nat.agda

@@ -9,7 +9,7 @@
 module Data.Star.Nat where
 
 open import Data.Unit
-open import Function
+open import Function.Base using (const)
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 open import Relation.Binary.Construct.Always using (Always)

src/Data/String.agda

@@ -21,7 +21,6 @@ open import Data.List.Relation.Binary.Lex.Strict using (Lex-<; Lex-≤)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Char.Base as Char using (Char)
 import Data.Char.Properties as Char using (_≟_)
-open import Function
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Nullary.Decidable using (does)

src/Data/Sum/Effectful/Examples.agda

@@ -21,7 +21,7 @@ private
   module Examplesₗ {a b} {A : Set a} {B : Set b} where
 
     open import Agda.Builtin.Equality
-    open import Function
+    open import Function.Base using (id)
     module Sₗ = Sumₗ A b
 
     open RawFunctor Sₗ.functor