diff --git a/README/Data/Container/Indexed.agda b/README/Data/Container/Indexed.agda
index 0c94e182ec..7ace9736f1 100644
--- a/README/Data/Container/Indexed.agda
+++ b/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
diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
index 38bb52d489..cb41cf41ef 100644
--- a/README/Design/Decidability.agda
+++ b/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
 
diff --git a/README/Function/Reasoning.agda b/README/Function/Reasoning.agda
index 0c9afa4532..4b9835346e 100644
--- a/README/Function/Reasoning.agda
+++ b/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
diff --git a/README/Nary.agda b/README/Nary.agda
index da2c2fcca3..16e50392b3 100644
--- a/README/Nary.agda
+++ b/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
diff --git a/README/Tactic/RingSolver.agda b/README/Tactic/RingSolver.agda
index fdbea87bbf..8071bee39c 100644
--- a/README/Tactic/RingSolver.agda
+++ b/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_)
diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
index 9cdad57edc..88a5cc5518 100644
--- a/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
+++ b/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
 
diff --git a/src/Algebra/Properties/AbelianGroup.agda b/src/Algebra/Properties/AbelianGroup.agda
index a1c2056ccb..6846f29d83 100644
--- a/src/Algebra/Properties/AbelianGroup.agda
+++ b/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
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
index e103b7a70e..5bc696da38 100644
--- a/src/Algebra/Solver/Ring.agda
+++ b/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_
diff --git a/src/Algebra/Solver/Ring/Lemmas.agda b/src/Algebra/Solver/Ring/Lemmas.agda
index 0a9cd7ac73..944e30dfb7 100644
--- a/src/Algebra/Solver/Ring/Lemmas.agda
+++ b/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)
diff --git a/src/Axiom/Extensionality/Heterogeneous.agda b/src/Axiom/Extensionality/Heterogeneous.agda
index 0b10affb61..ed1be68791 100644
--- a/src/Axiom/Extensionality/Heterogeneous.agda
+++ b/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
diff --git a/src/Codata/Sized/Delay/Effectful.agda b/src/Codata/Sized/Delay/Effectful.agda
index 95254c3a13..2724c67d47 100644
--- a/src/Codata/Sized/Delay/Effectful.agda
+++ b/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
diff --git a/src/Data/Container/Relation/Binary/Pointwise.agda b/src/Data/Container/Relation/Binary/Pointwise.agda
index 2b0b966b3d..7b20aa8dbb 100644
--- a/src/Data/Container/Relation/Binary/Pointwise.agda
+++ b/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
diff --git a/src/Data/Container/Relation/Unary/Any.agda b/src/Data/Container/Relation/Unary/Any.agda
index 944734af3d..de3937f221 100644
--- a/src/Data/Container/Relation/Unary/Any.agda
+++ b/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
diff --git a/src/Data/DifferenceList.agda b/src/Data/DifferenceList.agda
index dc62baf000..3227e6ed8e 100644
--- a/src/Data/DifferenceList.agda
+++ b/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
diff --git a/src/Data/DifferenceNat.agda b/src/Data/DifferenceNat.agda
index 0d6c024e51..c0f33a1fea 100644
--- a/src/Data/DifferenceNat.agda
+++ b/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 _+_
 
diff --git a/src/Data/DifferenceVec.agda b/src/Data/DifferenceVec.agda
index acb50ffde0..c34382a051 100644
--- a/src/Data/DifferenceVec.agda
+++ b/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 _∷_ _++_
diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda
index d7b298f0ef..586b28e278 100644
--- a/src/Data/Graph/Acyclic.agda
+++ b/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 (_≡_)
 
diff --git a/src/Data/Integer/Divisibility.agda b/src/Data/Integer/Divisibility.agda
index 44a97c6554..0f089b30fc 100644
--- a/src/Data/Integer/Divisibility.agda
+++ b/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 ℕ
diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda
index d4a22e420a..db80bcb3a0 100644
--- a/src/Data/Integer/Divisibility/Signed.agda
+++ b/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
diff --git a/src/Data/List/NonEmpty/Effectful.agda b/src/Data/List/NonEmpty/Effectful.agda
index 654002c839..373ceceb26 100644
--- a/src/Data/List/NonEmpty/Effectful.agda
+++ b/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
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index c4cf722ec6..c05d3251de 100644
--- a/src/Data/List/Properties.agda
+++ b/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
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda
index 563adfc9d9..ba61947c85 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda
+++ b/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)
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
index f66628a628..cdd8f968aa 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
+++ b/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
diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
index f3feaf2f02..78a365324b 100644
--- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
+++ b/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 (_≡_)
diff --git a/src/Data/List/Relation/Unary/First.agda b/src/Data/List/Relation/Unary/First.agda
index 90b8bf26cb..931195aea6 100644
--- a/src/Data/List/Relation/Unary/First.agda
+++ b/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
 
diff --git a/src/Data/List/Relation/Unary/First/Properties.agda b/src/Data/List/Relation/Unary/First/Properties.agda
index 7885712d7e..f30e037022 100644
--- a/src/Data/List/Relation/Unary/First/Properties.agda
+++ b/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
diff --git a/src/Data/List/Reverse.agda b/src/Data/List/Reverse.agda
index 92b2aa5b0c..0464181932 100644
--- a/src/Data/List/Reverse.agda
+++ b/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
diff --git a/src/Data/List/Zipper.agda b/src/Data/List/Zipper.agda
index 86f122e522..e2cc769ed2 100644
--- a/src/Data/List/Zipper.agda
+++ b/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
diff --git a/src/Data/List/Zipper/Properties.agda b/src/Data/List/Zipper/Properties.agda
index 3e3dea85d2..5c4ce7c7d8 100644
--- a/src/Data/List/Zipper/Properties.agda
+++ b/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
 ------------------------------------------------------------------------
diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda
index 6833f301e7..cb19c9c328 100644
--- a/src/Data/Maybe/Properties.agda
+++ b/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
diff --git a/src/Data/Maybe/Relation/Unary/All/Properties.agda b/src/Data/Maybe/Relation/Unary/All/Properties.agda
index 37d55adf0a..493f8679d0 100644
--- a/src/Data/Maybe/Relation/Unary/All/Properties.agda
+++ b/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
diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index 13701b486c..04283143fd 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/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)
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index 9e21f6f812..c843ae215b 100644
--- a/src/Data/Nat/GCD.agda
+++ b/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
diff --git a/src/Data/Nat/GCD/Lemmas.agda b/src/Data/Nat/GCD/Lemmas.agda
index 8d92924ddd..3f9a4b6d42 100644
--- a/src/Data/Nat/GCD/Lemmas.agda
+++ b/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
diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index ba4dc24f1d..9e89841633 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/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)
diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda
index 5ce1c7cd2a..af85ed64ad 100644
--- a/src/Data/Nat/LCM.agda
+++ b/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
diff --git a/src/Data/Product/Effectful/Examples.agda b/src/Data/Product/Effectful/Examples.agda
index daf05ce431..a393cb4f66 100644
--- a/src/Data/Product/Effectful/Examples.agda
+++ b/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)
diff --git a/src/Data/Product/Properties/WithK.agda b/src/Data/Product/Properties/WithK.agda
index 2218ec4ca3..645ea6a6c4 100644
--- a/src/Data/Product/Properties/WithK.agda
+++ b/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
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Record.agda b/src/Data/Record.agda
index b2328e89ad..edc19da8ff 100644
--- a/src/Data/Record.agda
+++ b/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
diff --git a/src/Data/Star/BoundedVec.agda b/src/Data/Star/BoundedVec.agda
index bae0c52f2d..2755554354 100644
--- a/src/Data/Star/BoundedVec.agda
+++ b/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
diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda
index 170b5abb07..48c0f4f11a 100644
--- a/src/Data/Star/Decoration.agda
+++ b/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
diff --git a/src/Data/Star/Nat.agda b/src/Data/Star/Nat.agda
index 42cf1e6b9f..ef81051ff9 100644
--- a/src/Data/Star/Nat.agda
+++ b/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)
diff --git a/src/Data/String.agda b/src/Data/String.agda
index 7ff82dfac0..8a6dd08045 100644
--- a/src/Data/String.agda
+++ b/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)
diff --git a/src/Data/Sum/Effectful/Examples.agda b/src/Data/Sum/Effectful/Examples.agda
index f6850c7e19..773c6ca316 100644
--- a/src/Data/Sum/Effectful/Examples.agda
+++ b/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
diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda
index 3fede95b06..2c6e638731 100644
--- a/src/Data/Sum/Properties.agda
+++ b/src/Data/Sum/Properties.agda
@@ -10,8 +10,8 @@ module Data.Sum.Properties where
 
 open import Level
 open import Data.Sum.Base
-open import Function
-open import Function.Bundles using (mk↔′)
+open import Function.Base using (_∋_; _∘_; id)
+open import Function.Bundles using (mk↔′; _↔_)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
index 34c676bcbb..2749640316 100644
--- a/src/Data/Sum/Relation/Binary/LeftOrder.agda
+++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda
@@ -13,7 +13,7 @@ open import Data.Sum.Relation.Binary.Pointwise as PW
   using (Pointwise; inj₁; inj₂)
 open import Data.Product
 open import Data.Empty
-open import Function
+open import Function.Base using (_$_; _∘_)
 open import Level
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
diff --git a/src/Data/These.agda b/src/Data/These.agda
index c8d042c8e9..45024ec599 100644
--- a/src/Data/These.agda
+++ b/src/Data/These.agda
@@ -11,7 +11,7 @@ module Data.These where
 open import Level
 open import Data.Maybe.Base using (Maybe; just; nothing; maybe′)
 open import Data.Sum.Base using (_⊎_; [_,_]′)
-open import Function
+open import Function.Base using (const; _∘′_; id; constᵣ)
 
 
 ------------------------------------------------------------------------
diff --git a/src/Data/These/Effectful/Left/Base.agda b/src/Data/These/Effectful/Left/Base.agda
index 04f569abdf..8f8f3c48bc 100644
--- a/src/Data/These/Effectful/Left/Base.agda
+++ b/src/Data/These/Effectful/Left/Base.agda
@@ -21,7 +21,7 @@ open import Data.These.Base
 open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad
-open import Function
+open import Function.Base using (_∘_; flip)
 
 Theseₗ : Set (a ⊔ b) → Set (a ⊔ b)
 Theseₗ B = These A B
diff --git a/src/Data/These/Effectful/Right/Base.agda b/src/Data/These/Effectful/Right/Base.agda
index 91da52ab02..721426ae68 100644
--- a/src/Data/These/Effectful/Right/Base.agda
+++ b/src/Data/These/Effectful/Right/Base.agda
@@ -21,7 +21,7 @@ open import Data.These.Base
 open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad
-open import Function
+open import Function.Base using (flip; _∘_)
 
 Theseᵣ : Set (a ⊔ b) → Set (a ⊔ b)
 Theseᵣ A = These A B
diff --git a/src/Data/Tree/AVL/NonEmpty.agda b/src/Data/Tree/AVL/NonEmpty.agda
index 622e2b4a58..d4af2edd58 100644
--- a/src/Data/Tree/AVL/NonEmpty.agda
+++ b/src/Data/Tree/AVL/NonEmpty.agda
@@ -23,7 +23,7 @@ open import Data.Maybe.Base hiding (map)
 open import Data.Nat.Base hiding (_<_; _⊔_; compare)
 open import Data.Product hiding (map)
 open import Data.Unit
-open import Function
+open import Function.Base using (_$_; _∘′_)
 open import Level using (_⊔_; Lift; lift)
 open import Relation.Unary
 
diff --git a/src/Data/Tree/Binary/Relation/Unary/All/Properties.agda b/src/Data/Tree/Binary/Relation/Unary/All/Properties.agda
index 198964ef4d..08361f8476 100644
--- a/src/Data/Tree/Binary/Relation/Unary/All/Properties.agda
+++ b/src/Data/Tree/Binary/Relation/Unary/All/Properties.agda
@@ -12,7 +12,7 @@ open import Level
 open import Data.Tree.Binary as Tree using (Tree; leaf; node)
 open import Data.Tree.Binary.Relation.Unary.All
 open import Relation.Unary
-open import Function
+open import Function.Base using (id)
 
 private
   variable
diff --git a/src/Data/Tree/Binary/Zipper.agda b/src/Data/Tree/Binary/Zipper.agda
index 0e5f4b8d05..5786ca7672 100644
--- a/src/Data/Tree/Binary/Zipper.agda
+++ b/src/Data/Tree/Binary/Zipper.agda
@@ -13,7 +13,7 @@ open import Data.Tree.Binary as BT using (Tree; node; leaf)
 open import Data.List.Base as List using (List; []; _∷_; sum; _++_; [_])
 open import Data.Maybe using (Maybe; nothing; just)
 open import Data.Nat.Base using (ℕ; suc; _+_)
-open import Function
+open import Function.Base using (_$_; _∘_)
 
 private
   variable
diff --git a/src/Data/Tree/Binary/Zipper/Properties.agda b/src/Data/Tree/Binary/Zipper/Properties.agda
index 20017ad162..107981bcbf 100644
--- a/src/Data/Tree/Binary/Zipper/Properties.agda
+++ b/src/Data/Tree/Binary/Zipper/Properties.agda
@@ -17,7 +17,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_; _∘_; _$_)
 open import Level using (Level)
 
 private
diff --git a/src/Data/Trie.agda b/src/Data/Trie.agda
index 2ea6b2f963..7f06a6f0ed 100644
--- a/src/Data/Trie.agda
+++ b/src/Data/Trie.agda
@@ -20,7 +20,7 @@ import Data.List.NonEmpty as List⁺
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe′)
 open import Data.Product as Prod using (∃)
 open import Data.These.Base as These using (These)
-open import Function
+open import Function.Base using (_∘′_; const)
 open import Relation.Unary using (IUniversal; _⇒_)
 
 open StrictTotalOrder S
diff --git a/src/Data/Universe/Indexed.agda b/src/Data/Universe/Indexed.agda
index a11958e16f..cb6d9f4e56 100644
--- a/src/Data/Universe/Indexed.agda
+++ b/src/Data/Universe/Indexed.agda
@@ -10,7 +10,7 @@ module Data.Universe.Indexed where
 
 open import Data.Product
 open import Data.Universe
-open import Function
+open import Function.Base using (_∘_)
 open import Level
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Bounded.agda b/src/Data/Vec/Bounded.agda
index 2e1f286419..3a1aae623e 100644
--- a/src/Data/Vec/Bounded.agda
+++ b/src/Data/Vec/Bounded.agda
@@ -11,7 +11,7 @@ module Data.Vec.Bounded where
 open import Level using (Level)
 open import Data.Nat.Base
 open import Data.Vec as Vec using (Vec)
-open import Function
+open import Function.Base using (id)
 open import Relation.Binary using (_Preserves_⟶_)
 open import Relation.Unary using (Pred; Decidable)
 
diff --git a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
index 3de5f61679..89dba8d259 100644
--- a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
@@ -14,7 +14,7 @@ open import Data.Product as Σ using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Functional as VF hiding (map)
 open import Data.Vec.Functional.Relation.Unary.All
-open import Function
+open import Function.Base using (const; _∘_)
 open import Level using (Level)
 open import Relation.Unary
 
diff --git a/src/Data/Vec/Functional/Relation/Unary/Any.agda b/src/Data/Vec/Functional/Relation/Unary/Any.agda
index 83e0e6dfb3..de6c3570cb 100644
--- a/src/Data/Vec/Functional/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Functional/Relation/Unary/Any.agda
@@ -13,7 +13,7 @@ open import Data.Fin.Properties using (any?)
 open import Data.Nat.Base
 open import Data.Product as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Functional as VF hiding (map)
-open import Function
+open import Function.Base using (id)
 open import Level using (Level)
 open import Relation.Unary
 
diff --git a/src/Data/Vec/Membership/Setoid.agda b/src/Data/Vec/Membership/Setoid.agda
index 1151aecf6f..50ef16bb79 100644
--- a/src/Data/Vec/Membership/Setoid.agda
+++ b/src/Data/Vec/Membership/Setoid.agda
@@ -10,7 +10,7 @@ open import Relation.Binary using (Setoid; _Respects_)
 
 module Data.Vec.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
-open import Function
+open import Function.Base using (_∘_; flip)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Any as Any
   using (Any; here; there; index)
diff --git a/src/Data/Vec/Recursive/Effectful.agda b/src/Data/Vec/Recursive/Effectful.agda
index 567020352a..cc58d5af6d 100644
--- a/src/Data/Vec/Recursive/Effectful.agda
+++ b/src/Data/Vec/Recursive/Effectful.agda
@@ -14,7 +14,7 @@ open import Data.Vec.Recursive
 open import Effect.Functor
 open import Effect.Applicative
 open import Effect.Monad
-open import Function
+open import Function.Base using (_∘_; flip)
 
 ------------------------------------------------------------------------
 -- Functor and applicative
diff --git a/src/Data/Word/Base.agda b/src/Data/Word/Base.agda
index 34206371e1..1dcaea5731 100644
--- a/src/Data/Word/Base.agda
+++ b/src/Data/Word/Base.agda
@@ -10,7 +10,7 @@ module Data.Word.Base where
 
 open import Level using (zero)
 import Data.Nat.Base as ℕ
-open import Function
+open import Function.Base using (_on_)
 open import Relation.Binary using (Rel)
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Effect/Applicative/Predicate.agda b/src/Effect/Applicative/Predicate.agda
index 0bfe6a9803..bcfec53170 100644
--- a/src/Effect/Applicative/Predicate.agda
+++ b/src/Effect/Applicative/Predicate.agda
@@ -13,7 +13,7 @@ module Effect.Applicative.Predicate where
 
 open import Effect.Functor.Predicate
 open import Data.Product
-open import Function
+open import Function.Base using (const; constᵣ)
 open import Level
 open import Relation.Unary
 open import Relation.Unary.PredicateTransformer using (Pt)
diff --git a/src/Effect/Comonad.agda b/src/Effect/Comonad.agda
index 67a4d7d43d..72cf07d732 100644
--- a/src/Effect/Comonad.agda
+++ b/src/Effect/Comonad.agda
@@ -11,7 +11,7 @@
 module Effect.Comonad where
 
 open import Level
-open import Function
+open import Function.Base using (id; _∘′_; flip)
 
 private
   variable
diff --git a/src/Effect/Functor/Predicate.agda b/src/Effect/Functor/Predicate.agda
index d24938b26a..70704e34c3 100644
--- a/src/Effect/Functor/Predicate.agda
+++ b/src/Effect/Functor/Predicate.agda
@@ -10,7 +10,7 @@
 
 module Effect.Functor.Predicate where
 
-open import Function
+open import Function.Base using (const)
 open import Level
 open import Relation.Unary
 open import Relation.Unary.PredicateTransformer using (PT)
diff --git a/src/Effect/Monad/Continuation.agda b/src/Effect/Monad/Continuation.agda
index bcc66ce265..2ff9dd4bb9 100644
--- a/src/Effect/Monad/Continuation.agda
+++ b/src/Effect/Monad/Continuation.agda
@@ -13,7 +13,7 @@ open import Effect.Applicative.Indexed
 open import Effect.Monad
 open import Function.Identity.Effectful as Id using (Identity)
 open import Effect.Monad.Indexed
-open import Function
+open import Function.Base using (flip)
 open import Level
 
 private
diff --git a/src/Effect/Monad/Partiality/All.agda b/src/Effect/Monad/Partiality/All.agda
index 7e90400a85..2954a5da2b 100644
--- a/src/Effect/Monad/Partiality/All.agda
+++ b/src/Effect/Monad/Partiality/All.agda
@@ -11,7 +11,7 @@ module Effect.Monad.Partiality.All where
 open import Effect.Monad
 open import Effect.Monad.Partiality as Partiality using (_⊥; ⇒≈)
 open import Codata.Musical.Notation
-open import Function
+open import Function.Base using (flip; _∘_)
 open import Level
 open import Relation.Binary using (_Respects_; IsEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
diff --git a/src/Effect/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda
index 5593b202d8..df3e58347c 100644
--- a/src/Effect/Monad/Predicate.agda
+++ b/src/Effect/Monad/Predicate.agda
@@ -15,7 +15,7 @@ open import Effect.Monad
 open import Effect.Monad.Indexed
 open import Data.Unit
 open import Data.Product
-open import Function
+open import Function.Base using (const; id; _∘_)
 open import Level
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary
diff --git a/src/Effect/Monad/Reader/Indexed.agda b/src/Effect/Monad/Reader/Indexed.agda
index 2260b07e09..28eab8d453 100644
--- a/src/Effect/Monad/Reader/Indexed.agda
+++ b/src/Effect/Monad/Reader/Indexed.agda
@@ -10,7 +10,7 @@ open import Level
 
 module Effect.Monad.Reader.Indexed {r} (R : Set r) (a : Level) where
 
-open import Function
+open import Function.Base using (const; flip; _∘_)
 open import Function.Identity.Effectful as Id using (Identity)
 open import Effect.Applicative.Indexed
 open import Effect.Monad.Indexed
diff --git a/src/Effect/Monad/Writer/Indexed.agda b/src/Effect/Monad/Writer/Indexed.agda
index 9720e72b3c..6d99dd9b43 100644
--- a/src/Effect/Monad/Writer/Indexed.agda
+++ b/src/Effect/Monad/Writer/Indexed.agda
@@ -16,7 +16,7 @@ open import Data.Unit.Polymorphic
 open import Effect.Applicative.Indexed
 open import Effect.Monad
 open import Effect.Monad.Indexed
-open import Function
+open import Function.Base using (_∘′_)
 open import Function.Identity.Effectful as Id using (Identity)
 
 private
diff --git a/src/Function/Construct/Composition.agda b/src/Function/Construct/Composition.agda
index a18b4b87b1..269448eaba 100644
--- a/src/Function/Construct/Composition.agda
+++ b/src/Function/Construct/Composition.agda
@@ -9,7 +9,13 @@
 module Function.Construct.Composition where
 
 open import Data.Product.Base using (_,_)
-open import Function
+open import Function.Base using (_∘_)
+open import Function.Bundles
+  using (Func; Injection; Surjection; Bijection; Equivalence; LeftInverse; RightInverse; Inverse; _⟶_; _↣_; _↠_; _⤖_; _⇔_; _↩_; _↪_; _↔_)
+open import Function.Definitions
+  using (Congruent; Injective; Surjective; Bijective; Inverseˡ; Inverseʳ; Inverseᵇ)
+open import Function.Structures
+  using (IsCongruent; IsInjection; IsSurjection; IsBijection; IsLeftInverse; IsRightInverse; IsInverse)
 open import Level using (Level)
 open import Relation.Binary hiding (_⇔_; IsEquivalence)
 
diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda
index 1974dee391..14a7adc466 100644
--- a/src/Function/Construct/Symmetry.agda
+++ b/src/Function/Construct/Symmetry.agda
@@ -9,7 +9,13 @@
 module Function.Construct.Symmetry where
 
 open import Data.Product.Base using (_,_; swap; proj₁; proj₂)
-open import Function
+open import Function.Base using (_∘_)
+open import Function.Definitions
+  using (Bijective; Injective; Surjective; Inverseˡ; Inverseʳ; Inverseᵇ; Congruent)
+open import Function.Structures
+  using (IsBijection; IsCongruent; IsRightInverse; IsLeftInverse; IsInverse)
+open import Function.Bundles
+  using (Bijection; Equivalence; LeftInverse; RightInverse; Inverse; _⤖_; _⇔_; _↩_; _↪_; _↔_)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Symmetric; Transitive)
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index d14128edfe..9cb46af85f 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -18,7 +18,7 @@ open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Nat.Properties using (+-0-monoid; +-semigroup)
 open import Data.Product using (_,_)
 
-open import Function
+open import Function.Base using (id; _∘′_; _∋_)
 open import Function.Equality using (_⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
diff --git a/src/Function/Properties.agda b/src/Function/Properties.agda
index b20807f64e..adfb3c73b6 100644
--- a/src/Function/Properties.agda
+++ b/src/Function/Properties.agda
@@ -9,7 +9,8 @@
 module Function.Properties where
 
 open import Axiom.Extensionality.Propositional using (Extensionality)
-open import Function
+open import Function.Base using (flip; _∘_)
+open import Function.Bundles using (_↔_; mk↔′; Inverse)
 open import Level
 open import Relation.Binary.PropositionalEquality.Core
   using (trans; cong; cong′)
diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
index 64c81b7151..963c5b6330 100644
--- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
+++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
@@ -8,7 +8,7 @@
 
 module Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties where
 
-open import Function
+open import Function.Base using (id; _∘_; _$_)
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 open import Relation.Binary.PropositionalEquality.Core as PropEq
diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda
index c88cf76c8a..aa2fd6e0a5 100644
--- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda
+++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda
@@ -11,7 +11,7 @@ module
   Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties.WithK
   where
 
-open import Function
+open import Function.Base using (_∋_)
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda b/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda
index 62816238d9..b432e3e1dd 100644
--- a/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda
+++ b/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda
@@ -8,7 +8,7 @@
 
 module Relation.Binary.Construct.Closure.Transitive.WithK where
 
-open import Function
+open import Function.Base using (_∋_)
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.Transitive
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients.agda
index a429dafe8f..fcdc1e97fc 100644
--- a/src/Relation/Binary/HeterogeneousEquality/Quotients.agda
+++ b/src/Relation/Binary/HeterogeneousEquality/Quotients.agda
@@ -8,7 +8,7 @@
 
 module Relation.Binary.HeterogeneousEquality.Quotients where
 
-open import Function
+open import Function.Base using (_$_; const; _∘_)
 open import Level hiding (lift)
 open import Relation.Binary
 open import Relation.Binary.HeterogeneousEquality
diff --git a/src/Relation/Nullary/Indexed/Negation.agda b/src/Relation/Nullary/Indexed/Negation.agda
index 45c6a9e2a1..4a742baea3 100644
--- a/src/Relation/Nullary/Indexed/Negation.agda
+++ b/src/Relation/Nullary/Indexed/Negation.agda
@@ -10,7 +10,7 @@ module Relation.Nullary.Indexed.Negation where
 
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Empty.Polymorphic
-open import Function
+open import Function.Bundles using (_↔_)
 open import Function.Properties
 import Function.Construct.Identity as Identity
 open import Relation.Nullary.Indexed
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index 6ab36647c3..5df3c1c423 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -21,7 +21,7 @@ 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
-open import Function
+open import Function.Base using (_∘_; id)
 import Function.Equality as FunS
 open import Data.Empty
 open import Effect.Applicative
diff --git a/src/Relation/Unary/PredicateTransformer.agda b/src/Relation/Unary/PredicateTransformer.agda
index b6df4f2b8a..0ae725588a 100644
--- a/src/Relation/Unary/PredicateTransformer.agda
+++ b/src/Relation/Unary/PredicateTransformer.agda
@@ -9,7 +9,7 @@
 module Relation.Unary.PredicateTransformer where
 
 open import Data.Product
-open import Function
+open import Function.Base using (_∘_)
 open import Level hiding (_⊔_)
 open import Relation.Nullary
 open import Relation.Unary
diff --git a/src/System/Directory.agda b/src/System/Directory.agda
index baee50bc2d..fc2a1578a9 100644
--- a/src/System/Directory.agda
+++ b/src/System/Directory.agda
@@ -17,7 +17,7 @@ open import Data.Maybe.Base using (Maybe)
 open import Data.Nat.Base using (ℕ)
 open import Data.String.Base using (String)
 open import Foreign.Haskell.Coerce using (coerce)
-open import Function
+open import Function.Base using (_∘′_)
 open import System.FilePath.Posix hiding (makeRelative)
 
 open import System.Directory.Primitive as Prim
diff --git a/src/System/FilePath/Posix.agda b/src/System/FilePath/Posix.agda
index 4e4a205d47..d486f1d342 100644
--- a/src/System/FilePath/Posix.agda
+++ b/src/System/FilePath/Posix.agda
@@ -15,7 +15,6 @@ open import IO.Base using (IO; lift)
 open import Data.Maybe.Base using (Maybe)
 open import Data.Product using (_×_)
 open import Data.Sum.Base using (_⊎_)
-open import Function
 
 open import Foreign.Haskell.Coerce
 
diff --git a/src/Tactic/MonoidSolver.agda b/src/Tactic/MonoidSolver.agda
index fcf193244b..991ff41556 100644
--- a/src/Tactic/MonoidSolver.agda
+++ b/src/Tactic/MonoidSolver.agda
@@ -73,7 +73,7 @@
 module Tactic.MonoidSolver where
 
 open import Algebra
-open import Function
+open import Function.Base using (_⟨_⟩_)
 
 open import Data.Bool         as Bool    using (Bool; _∨_; if_then_else_)
 open import Data.Maybe        as Maybe   using (Maybe; just; nothing; maybe)
diff --git a/src/Tactic/RingSolver/Core/NatSet.agda b/src/Tactic/RingSolver/Core/NatSet.agda
index 7ebbcebc22..d28b441d05 100644
--- a/src/Tactic/RingSolver/Core/NatSet.agda
+++ b/src/Tactic/RingSolver/Core/NatSet.agda
@@ -40,7 +40,7 @@ open import Data.Nat        as ℕ     using (ℕ; suc; zero)
 open import Data.List.Base  as List  using (List; _∷_; [])
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Bool       as Bool  using (Bool)
-open import Function
+open import Function.Base            using (const; _∘_)
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
index 1eb2244f5d..1f6de95f4f 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
@@ -19,7 +19,7 @@ open import Data.Product              using (_,_; _×_; proj₂)
 open import Data.List.Base            using (_∷_; [])
 open import Data.List.Kleene
 open import Data.Vec                  using (Vec)
-open import Function
+open import Function.Base using (_⟨_⟩_; flip)
 open import Relation.Unary
 
 import Relation.Binary.PropositionalEquality.Core as ≡
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
index ca622ab00a..9435251957 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
@@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Function
+open import Function.Base using (_⟨_⟩_)
 
 open import Data.Nat.Base as ℕ using (ℕ; suc; zero; compare)
 open import Data.Product  using (_,_; _×_; proj₁; proj₂)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
index 6f2eba31d7..3e1ce2bfe3 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
@@ -23,7 +23,7 @@ open import Data.Unit using (tt)
 open import Data.List.Kleene
 open import Data.Product                                    using (_,_; proj₁; proj₂; map₁; _×_)
 open import Data.Maybe                                      using (nothing; just)
-open import Function
+open import Function.Base                                   using (_⟨_⟩_)
 open import Level                                           using (lift)
 open import Relation.Nullary                                using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
index c322284a96..2baeac0f23 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
@@ -19,7 +19,7 @@ open import Data.Nat.Induction
 open import Data.Product           using (_×_; _,_; proj₁; proj₂; map₁)
 open import Data.List.Kleene
 open import Data.Vec               using (Vec)
-open import Function
+open import Function.Base using (_⟨_⟩_; flip)
 open import Induction.WellFounded
 open import Relation.Unary
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
index ebef6fc39e..dd84eafef2 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
@@ -18,7 +18,7 @@ open import Data.Vec              using (Vec)
 open import Data.Nat              using (_<′_)
 open import Data.Nat.Induction
 
-open import Function
+open import Function.Base using (_⟨_⟩_; flip)
 
 open Homomorphism homo
 open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Parameters.agda b/src/Tactic/RingSolver/Core/Polynomial/Parameters.agda
index a622ffb49c..c7777160a8 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Parameters.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Parameters.agda
@@ -13,7 +13,6 @@ module Tactic.RingSolver.Core.Polynomial.Parameters where
 
 open import Algebra.Bundles using (RawRing)
 open import Data.Bool.Base using (Bool; T)
-open import Function
 open import Level
 open import Relation.Unary
 open import Tactic.RingSolver.Core.AlmostCommutativeRing
diff --git a/src/Tactic/RingSolver/NonReflective.agda b/src/Tactic/RingSolver/NonReflective.agda
index 1c65a6c1bb..ef99adc22e 100644
--- a/src/Tactic/RingSolver/NonReflective.agda
+++ b/src/Tactic/RingSolver/NonReflective.agda
@@ -18,7 +18,7 @@ module Tactic.RingSolver.NonReflective
   where
 
 open import Algebra.Morphism
-open import Function
+open import Function.Base using (id; _⟨_⟩_)
 open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
 open import Data.Maybe.Base
 open import Data.Empty using (⊥-elim)