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: 2 people

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