diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda
index fde96b9..121cb24 100644
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@@ -7,7 +7,6 @@ open import Data.Bool hiding (T)
 open import Data.Sum hiding ([_,_])
 open import Data.Unit
 open import Data.Empty
-open import Function
 open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index a0b4d1d..157b3b5 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -2,7 +2,6 @@
 module Cat.Categories.Fam where
 
 open import Cat.Prelude
-import Function
 
 open import Cat.Category
 
@@ -15,7 +14,7 @@ module _ (ℓa ℓb : Level) where
     fst identity = λ x → x
     snd identity = λ b → b
     _<<<_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
-    (g , g') <<< (f , f') = g Function.∘ f , g' Function.∘ f'
+    (g , g') <<< (f , f') = g ∘ f , g' ∘ f'
 
     RawFam : RawCategory (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb)
     RawFam = record
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 71c9044..3aa4e59 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -2,7 +2,6 @@
 module Cat.Categories.Rel where
 
 open import Cat.Prelude hiding (Rel)
-open import Function
 
 open import Cat.Category
 
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index f950339..b2ae61f 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -4,8 +4,6 @@ module Cat.Categories.Sets where
 
 open import Cat.Prelude as P
 
-open import Function using (_∘_ ; _∘′_)
-
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
@@ -25,14 +23,14 @@ module _ (ℓ : Level) where
     SetsRaw : RawCategory (lsuc ℓ) ℓ
     RawCategory.Object   SetsRaw = hSet ℓ
     RawCategory.Arrow    SetsRaw (T , _) (U , _) = T → U
-    RawCategory.identity SetsRaw = Function.id
-    RawCategory._<<<_    SetsRaw = Function._∘′_
+    RawCategory.identity SetsRaw = idFun _
+    RawCategory._<<<_    SetsRaw = _∘′_
 
     module _ where
       private
         open RawCategory SetsRaw hiding (_<<<_)
 
-        isIdentity : IsIdentity Function.id
+        isIdentity : IsIdentity (idFun _)
         fst isIdentity = funExt λ _ → refl
         snd isIdentity = funExt λ _ → refl
 
@@ -70,17 +68,17 @@ module _ (ℓ : Level) where
             where
             module xxA = AreInverses xx
             module yyA = AreInverses yy
-            ve-re : g ∘ f ≡ Function.id
+            ve-re : g ∘ f ≡ idFun _
             ve-re = arrowsAreSets {A = hA} {B = hA} _ _ xxA.verso-recto yyA.verso-recto i
-            re-ve : f ∘ g ≡ Function.id
+            re-ve : f ∘ g ≡ idFun _
             re-ve = arrowsAreSets {A = hB} {B = hB} _ _ xxA.recto-verso yyA.recto-verso i
           1eq : x.inverse ≡ y.inverse
           1eq = begin
             x.inverse                   ≡⟨⟩
-            x.inverse ∘ Function.id     ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩
+            x.inverse ∘ idFun _         ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩
             x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩
             (x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) xA.verso-recto ⟩
-            Function.id ∘ y.inverse     ≡⟨⟩
+            idFun _ ∘ y.inverse         ≡⟨⟩
             y.inverse                   ∎
           2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ]
           2eq = lemPropF p 1eq
@@ -266,7 +264,7 @@ module _ {ℓ : Level} where
         module _ (hX : Object) where
           open Σ hX renaming (fst to X)
           module _ (f : X → A ) (g : X → B) where
-            ump : fst Function.∘′ (f &&& g) ≡ f × snd Function.∘′ (f &&& g) ≡ g
+            ump : fst ∘′ (f &&& g) ≡ f × snd ∘′ (f &&& g) ≡ g
             fst ump = refl
             snd ump = refl
 
@@ -280,7 +278,7 @@ module _ {ℓ : Level} where
           = f &&& g , ump hX f g , λ eq → funExt (umpUniq eq)
           where
           open Σ hX renaming (fst to X) using ()
-          module _ {y : X → A × B} (eq : fst Function.∘′ y ≡ f × snd Function.∘′ y ≡ g) (x : X) where
+          module _ {y : X → A × B} (eq : fst ∘′ y ≡ f × snd ∘′ y ≡ g) (x : X) where
             p1 : fst ((f &&& g) x) ≡ fst (y x)
             p1 = begin
               fst ((f &&& g) x) ≡⟨⟩
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 6190052..428d357 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -35,8 +35,6 @@ open Cat.Equivalence
   renaming (_≅_ to _≈_)
   hiding (preorder≅ ; Isomorphism)
 
-import Function
-
 ------------------
 -- * Categories --
 ------------------
@@ -146,7 +144,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
     postulate from[Contr] : Univalent[Contr] → Univalent
 
     from[Andrea] : Univalent[Andrea] → Univalent
-    from[Andrea] = from[Contr] Function.∘ step
+    from[Andrea] = from[Contr] ∘ step
       where
       module _ (f : Univalent[Andrea]) (A : Object) where
         aux : isContr (Σ[ B ∈ Object ] A ≡ B)
@@ -510,7 +508,7 @@ module Opposite {ℓa ℓb : Level} where
         module ℂ = Category ℂ
         opRaw : RawCategory ℓa ℓb
         RawCategory.Object   opRaw = ℂ.Object
-        RawCategory.Arrow    opRaw = Function.flip ℂ.Arrow
+        RawCategory.Arrow    opRaw = flip ℂ.Arrow
         RawCategory.identity opRaw = ℂ.identity
         RawCategory._<<<_    opRaw = ℂ._>>>_
 
@@ -529,9 +527,6 @@ module Opposite {ℓa ℓb : Level} where
         open Σ k renaming (fst to η ; snd to inv-η)
         open AreInverses inv-η
 
-        _⊙_ = Function._∘_
-        infixr 9 _⊙_
-
         genericly : {ℓa ℓb ℓc : Level} {a : Set ℓa} {b : Set ℓb} {c : Set ℓc}
           → a × b × c → b × a × c
         genericly (a , b , c) = (b , a , c)
@@ -557,22 +552,22 @@ module Opposite {ℓa ℓb : Level} where
           open Σ r-iso renaming (fst to r-l ; snd to r-r)
 
         ζ : A ≅ B → A ≡ B
-        ζ = η ⊙ shuffle
+        ζ = η ∘ shuffle
 
         -- inv : AreInverses (ℂ.idToIso A B) f
         inv-ζ : AreInverses (idToIso A B) ζ
         -- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≅ B)
         inv-ζ = record
           { verso-recto = funExt (λ x → begin
-            (ζ ⊙ idToIso A B) x                       ≡⟨⟩
-            (η  ⊙ shuffle ⊙ idToIso A B) x             ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ⊙ shuffle ⊙ φ) (funExt lem)) ⟩
-            (η  ⊙ shuffle ⊙ shuffle~ ⊙ ℂ.idToIso A B) x ≡⟨⟩
-            (η  ⊙ ℂ.idToIso A B) x                     ≡⟨ (λ i → verso-recto i x) ⟩
+            (ζ ∘ idToIso A B) x                       ≡⟨⟩
+            (η  ∘ shuffle ∘ idToIso A B) x             ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ∘ shuffle ∘ φ) (funExt lem)) ⟩
+            (η  ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x ≡⟨⟩
+            (η  ∘ ℂ.idToIso A B) x                     ≡⟨ (λ i → verso-recto i x) ⟩
             x ∎)
           ; recto-verso = funExt (λ x → begin
-            (idToIso A B ⊙ η ⊙ shuffle) x             ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ⊙ η ⊙ shuffle) (funExt lem)) ⟩
-            (shuffle~ ⊙ ℂ.idToIso A B ⊙ η ⊙ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ⊙ φ ⊙ shuffle) recto-verso) ⟩
-            (shuffle~ ⊙ shuffle) x                       ≡⟨⟩
+            (idToIso A B ∘ η ∘ shuffle) x             ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ η ∘ shuffle) (funExt lem)) ⟩
+            (shuffle~ ∘ ℂ.idToIso A B ∘ η ∘ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩
+            (shuffle~ ∘ shuffle) x                       ≡⟨⟩
             x ∎)
           }
 
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 08dcafa..b94dff2 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -2,7 +2,6 @@
 module Cat.Category.Functor where
 
 open import Cat.Prelude
-open import Function
 
 open import Cubical
 
@@ -165,8 +164,8 @@ module Functors where
   module _ {ℓc ℓcc : Level} {ℂ : Category ℓc ℓcc} where
     private
       raw : RawFunctor ℂ ℂ
-      RawFunctor.omap raw = Function.id
-      RawFunctor.fmap raw = Function.id
+      RawFunctor.omap raw = idFun _
+      RawFunctor.fmap raw = idFun _
 
       isFunctor : IsFunctor ℂ ℂ raw
       IsFunctor.isIdentity     isFunctor = refl
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index f4dc465..3ba9653 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -5,7 +5,6 @@ This module provides construction 2.3 in [voe]
 module Cat.Category.Monad.Voevodsky where
 
 open import Cat.Prelude
-open import Function
 
 open import Cat.Category
 open import Cat.Category.Functor as F
@@ -132,10 +131,10 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       Kleisli→Monoidal : K.Monad → M.Monad
       Kleisli→Monoidal = E.reverse
 
-      ve-re : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ Function.id
+      ve-re : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ idFun _
       ve-re = E.verso-recto
 
-      re-ve : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id
+      re-ve : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ idFun _
       re-ve = E.recto-verso
 
       forth : §2-3.§1 omap pure → §2-3.§2 omap pure
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index caa993f..6ec32ba 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -3,7 +3,6 @@ module Cat.Category.Product where
 
 open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
 open import Cat.Equivalence hiding (_≅_)
--- module P = Cat.Prelude
 
 open import Cat.Category
 
@@ -203,15 +202,13 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         : ((X , xa , xb) ≡ (Y , ya , yb))
         ≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
       step0
-        = (λ p → cong fst p , cong-d (fst ⊙ snd) p , cong-d (snd ⊙ snd) p)
+        = (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
         -- , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
         , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
         , record
           { verso-recto = funExt (λ{ p → refl})
           ; recto-verso = funExt (λ{ (p , q , r) → refl})
           }
-          where
-          open import Function renaming (_∘_ to _⊙_)
 
       -- Should follow from c being univalent
       iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p)
diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index 43a25e4..4ca5a93 100644
--- a/src/Cat/Equivalence.agda
+++ b/src/Cat/Equivalence.agda
@@ -151,8 +151,6 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
             (x ∘ f) ∘ y   ≡⟨ cong (λ φ → φ ∘ y) inv-x.verso-recto ⟩
             y ∎
 
-          open import Cat.Prelude
-
           propInv : ∀ g → isProp (AreInverses f g)
           propInv g t u i = record { verso-recto = a i ; recto-verso = b i }
             where
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index 0646bf5..a3d34a4 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -9,7 +9,10 @@ open import Data.Product public
   renaming (∃! to ∃!≈)
   using (_×_ ; Σ-syntax ; swap)
 
--- TODO Import Data.Function under appropriate names.
+open import Function using (_∘_ ; _∘′_ ; _$_ ; case_of_ ; flip) public
+
+idFun : ∀ {a} (A : Set a) → A → A
+idFun A a = a
 
 open import Cubical public
 -- FIXME rename `gradLemma` to `fromIsomorphism` - perhaps just use wrapper