diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index dbd2b786f..2ff5d1f71 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -45,8 +45,8 @@ on:
 ########################################################################
 
 env:
-  AGDA_COMMIT: tags/v2.6.3
-  STDLIB_VERSION: 1.7.2
+  AGDA_COMMIT: tags/v2.6.4
+  STDLIB_VERSION: "2.0"
 
   GHC_VERSION: 8.10.7
   CABAL_VERSION: 3.6.2.0
diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib
index 5b19c405e..3f89afb89 100644
--- a/agda-categories.agda-lib
+++ b/agda-categories.agda-lib
@@ -1,3 +1,3 @@
 name: agda-categories
-depend: standard-library-1.7.2
+depend: standard-library-2.0
 include: src/
diff --git a/src/Categories/Adjoint.agda b/src/Categories/Adjoint.agda
index 466d8961c..f42782e54 100644
--- a/src/Categories/Adjoint.agda
+++ b/src/Categories/Adjoint.agda
@@ -7,16 +7,14 @@ open import Level
 
 open import Data.Product using (_,_; _×_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality using (Π; _⟶_)
-import Function.Inverse as FI
+open import Function.Bundles using (Inverse)
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
 -- be explicit in imports to 'see' where the information comes from
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Product using (Product; _⁂_)
-open import Categories.Category.Instance.Setoids
-open import Categories.Morphism
+open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Functor.Hom using (Hom[_][-,-])
@@ -91,23 +89,19 @@ record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ leve
   module Hom[-,R-] = Functor Hom[-,R-]
 
   -- Inverse is more 'categorical' than bijection defined via injection/surjection
-  Hom-inverse : ∀ A B → FI.Inverse (Hom[L-,-].F₀ (A , B)) (Hom[-,R-].F₀ (A , B))
+  Hom-inverse : ∀ A B → Inverse (Hom[L-,-].F₀ (A , B)) (Hom[-,R-].F₀ (A , B))
   Hom-inverse A B = record
-    { to = record
-      { _⟨$⟩_ = Ladjunct {A} {B}
-      ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈
-      }
-    ; from = record
-      { _⟨$⟩_ = Radjunct {A} {B}
-      ; cong = D.∘-resp-≈ʳ ∙ L.F-resp-≈
-      }
-    ; inverse-of = record
-      { left-inverse-of = λ _ → RLadjunct≈id
-      ; right-inverse-of = λ _ → LRadjunct≈id
+    { to = Ladjunct {A} {B}
+    ; to-cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈
+    ; from = Radjunct {A} {B}
+    ; from-cong = D.∘-resp-≈ʳ ∙ L.F-resp-≈
+    ; inverse = record
+      { fst = λ p → C.∘-resp-≈ˡ (R.F-resp-≈ p) C.HomReasoning.○ LRadjunct≈id
+      ; snd = λ p → D.∘-resp-≈ʳ (L.F-resp-≈ p) D.HomReasoning.○ RLadjunct≈id
       }
     }
 
-  module Hom-inverse {A} {B} = FI.Inverse (Hom-inverse A B)
+  module Hom-inverse {A} {B} = Inverse (Hom-inverse A B)
 
   op : Adjoint R.op L.op
   op = record
@@ -188,15 +182,15 @@ record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ leve
     Hom-NI = record
       { F⇒G = ntHelper record
         { η       = λ _ → record
-          { _⟨$⟩_ = λ f → lift (Ladjunct (lower f))
-          ; cong  = λ eq → lift (Ladjunct-resp-≈ (lower eq))
+          { to = λ f → lift (Ladjunct (lower f))
+          ; cong = λ eq → lift (Ladjunct-resp-≈ (lower eq))
           }
         ; commute = λ _ eq → lift $ Ladjunct-comm (lower eq)
         }
       ; F⇐G = ntHelper record
         { η       = λ _ → record
-          { _⟨$⟩_ = λ f → lift (Radjunct (lower f))
-          ; cong  = λ eq → lift (Radjunct-resp-≈ (lower eq))
+          { to = λ f → lift (Radjunct (lower f))
+          ; cong = λ eq → lift (Radjunct-resp-≈ (lower eq))
           }
         ; commute = λ _ eq → lift $ Radjunct-comm (lower eq)
         }
diff --git a/src/Categories/Adjoint/Compose.agda b/src/Categories/Adjoint/Compose.agda
index a67069171..b67717ec4 100644
--- a/src/Categories/Adjoint/Compose.agda
+++ b/src/Categories/Adjoint/Compose.agda
@@ -7,8 +7,6 @@ open import Level
 
 open import Data.Product using (_,_; _×_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality using (Π; _⟶_)
-import Function.Inverse as FI
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 
 -- be explicit in imports to 'see' where the information comes from
diff --git a/src/Categories/Adjoint/Equivalents.agda b/src/Categories/Adjoint/Equivalents.agda
index 7577ee376..a36e5fcd7 100644
--- a/src/Categories/Adjoint/Equivalents.agda
+++ b/src/Categories/Adjoint/Equivalents.agda
@@ -8,16 +8,15 @@ open import Level
 
 open import Data.Product using (_,_; _×_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality using (Π; _⟶_)
-import Function.Inverse as FI
+open import Function.Bundles using (Equivalence; LeftInverse; Func; _⟨$⟩_)
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 
 -- be explicit in imports to 'see' where the information comes from
 open import Categories.Adjoint using (Adjoint; _⊣_)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Product using (Product; _⁂_)
-open import Categories.Category.Instance.Setoids
-open import Categories.Morphism
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Morphism using (Iso)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Functor.Hom using (Hom[_][-,-])
@@ -50,11 +49,11 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
     Hom-NI′ : NaturalIsomorphism Hom[L-,-] Hom[-,R-]
     Hom-NI′ = record
       { F⇒G = ntHelper record
-        { η       = λ _ → Hom-inverse.to
+        { η       = λ _ → record { to = Hom-inverse.to ; cong = Hom-inverse.to-cong }
         ; commute = λ _ eq → Ladjunct-comm eq
         }
       ; F⇐G = ntHelper record
-        { η       = λ _ → Hom-inverse.from
+        { η       = λ _ → record { to = Hom-inverse.from ; cong = Hom-inverse.from-cong }
         ; commute = λ _ eq → Radjunct-comm eq
         }
       ; iso = λ _ → record
@@ -78,10 +77,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
     open NaturalIsomorphism Hni
     open NaturalTransformation
     open Functor
-    open Π
+    open Func
 
     private
-      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
+      unitη : ∀ X → Func (F₀ Hom[L-,-] (X , L.F₀ X)) (F₀ Hom[-,R-] (X , L.F₀ X))
       unitη X = ⇒.η (X , L.F₀ X)
 
       unit : NaturalTransformation idF (R ∘F L)
@@ -100,7 +99,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
               open HomReasoning
               open MR C
 
-      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
+      counitη : ∀ X → Func (F₀ Hom[-,R-] (R.F₀ X , X)) (F₀ Hom[L-,-] (R.F₀ X , X))
       counitη X = ⇐.η (R.F₀ X , X)
 
       counit : NaturalTransformation (L ∘F R) idF
@@ -160,7 +159,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
     module L = Functor L
     module R = Functor R
     open Functor
-    open Π
+    open Func
 
     Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
     Hom[L-,-] = LiftSetoids ℓ e ∘F Hom[ D ][-,-] ∘F (L.op ⁂ idF)
@@ -171,7 +170,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
   module _ (Hni : Hom[L-,-] ≃ Hom[-,R-]) where
     open NaturalIsomorphism Hni using (module ⇒; module ⇐; iso)
     private
-      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
+      unitη : ∀ X → Func (F₀ Hom[L-,-] (X , L.F₀ X)) (F₀ Hom[-,R-] (X , L.F₀ X))
       unitη X = ⇒.η (X , L.F₀ X)
 
       unit : NaturalTransformation idF (R ∘F L)
@@ -196,7 +195,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
               open HomReasoning
               open MR C
 
-      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
+      counitη : ∀ X → Func (F₀ Hom[-,R-] (R.F₀ X , X)) (F₀ Hom[L-,-] (R.F₀ X , X))
       counitη X = ⇐.η (R.F₀ X , X)
 
       counit : NaturalTransformation (L ∘F R) idF
diff --git a/src/Categories/Adjoint/Instance/0-Truncation.agda b/src/Categories/Adjoint/Instance/0-Truncation.agda
index 3d0a60b0e..248abef27 100644
--- a/src/Categories/Adjoint/Instance/0-Truncation.agda
+++ b/src/Categories/Adjoint/Instance/0-Truncation.agda
@@ -7,9 +7,10 @@ module Categories.Adjoint.Instance.0-Truncation where
 
 open import Level using (Lift)
 open import Data.Unit using (⊤)
-import Function
+open import Function.Base renaming (id to id→)
+open import Function.Bundles using (Func)
+import Function.Construct.Identity as Id
 open import Relation.Binary using (Setoid)
-open import Function.Equality using (Π) renaming (id to idΠ)
 
 open import Categories.Adjoint using (_⊣_)
 open import Categories.Category.Construction.0-Groupoid using (0-Groupoid)
@@ -26,7 +27,7 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (refl)
 Inclusion : ∀ {c ℓ} e → Functor (Setoids c ℓ) (Groupoids c ℓ e)
 Inclusion {c} {ℓ} e = record
   { F₀           = 0-Groupoid e
-  ; F₁           = λ f → record { F₀ = f ⟨$⟩_ ; F₁ = cong f }
+  ; F₁           = λ f → record { F₀ = to f; F₁ = cong f }
   ; identity     = refl
   ; homomorphism = refl
   ; F-resp-≈     = λ {S T f g} f≗g →
@@ -37,7 +38,7 @@ Inclusion {c} {ℓ} e = record
     ; F⇐G = record { η = λ _ → T.sym (f≗g S.refl) }
     }
   }
-  where open Π
+  where open Func
 
 -- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids
 
@@ -45,19 +46,19 @@ TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
 TruncAdj {o} {ℓ} {e} = record
   { unit   = unit
   ; counit = counit
-  ; zig    = Function.id
+  ; zig    = id→
   ; zag    = refl
   }
   where
-    open Π
+    open Func
     open Groupoid using (category)
 
     unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
     unit = record
-      { η           = λ _ → record { F₀ = Function.id ; F₁ = Function.id }
+      { η           = λ _ → record { F₀ = id→ ; F₁ = id→ }
       ; commute     = λ _ → refl
       ; sym-commute = λ _ → refl
       }
 
     counit : NaturalTransformation (Trunc ∘F Inclusion e) idF
-    counit = ntHelper record { η = λ S → idΠ ; commute = λ f → cong f }
+    counit = ntHelper record { η = Id.function; commute = λ f → cong f }
diff --git a/src/Categories/Adjoint/Instance/PosetCore.agda b/src/Categories/Adjoint/Instance/PosetCore.agda
index 78663a0a0..9bd939375 100644
--- a/src/Categories/Adjoint/Instance/PosetCore.agda
+++ b/src/Categories/Adjoint/Instance/PosetCore.agda
@@ -7,7 +7,7 @@ module Categories.Adjoint.Instance.PosetCore where
 
 open import Level using (_⊔_)
 import Function
-open import Function.Equality using (Π; _⟶_)
+open import Function.Bundles using (Func)
 open import Relation.Binary using (Setoid; Poset)
 open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)
 import Relation.Binary.Morphism.Construct.Composition as Comp
@@ -15,8 +15,8 @@ import Relation.Binary.Morphism.Construct.Composition as Comp
 open import Categories.Adjoint using (_⊣_)
 import Categories.Adjoint.Instance.0-Truncation as Setd
 import Categories.Adjoint.Instance.01-Truncation as Pos
-open import Categories.Category using (Category)
-open import Categories.Category.Construction.Thin
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Construction.Thin using (Thin; module EqIsIso)
 open import Categories.Category.Instance.Posets using (Posets)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor.Instance.Core using () renaming (Core to CatCore)
@@ -28,15 +28,16 @@ open import Categories.NaturalTransformation using (ntHelper)
 open import Categories.NaturalTransformation.NaturalIsomorphism
   using (_≃_; niHelper)
 
-open Π
 open PosetHomomorphism using (⟦_⟧; cong)
 
 -- The "forgetful" functor from Setoids to Posets (forgetting symmetry).
 
+open Func
+
 Forgetful : ∀ {c ℓ} → Functor (Setoids c ℓ) (Posets c ℓ ℓ)
 Forgetful = record
   { F₀           = Forgetful₀
-  ; F₁           = λ f → mkPosetHomo _ _ (f ⟨$⟩_) (cong f)
+  ; F₁           = λ f → mkPosetHomo _ _ (to f) (cong f)
   ; identity     = λ {S}       → refl S
   ; homomorphism = λ {_ _ S}   → refl S
   ; F-resp-≈     = λ {S _} f≗g → f≗g (refl S)
@@ -70,7 +71,7 @@ Forgetful = record
 Core : ∀ {c ℓ₁ ℓ₂} → Functor (Posets c ℓ₁ ℓ₂) (Setoids c ℓ₁)
 Core = record
   { F₀           = λ A → record { isEquivalence = isEquivalence A }
-  ; F₁           = λ f → record { _⟨$⟩_ = ⟦ f ⟧ ; cong = cong f }
+  ; F₁           = λ f → record { to = ⟦ f ⟧ ; cong = cong f }
   ; identity     = Function.id
   ; homomorphism = λ {_ _ _ f g} → cong (Comp.posetHomomorphism f g)
   ; F-resp-≈     = λ {_ B} {f _} f≗g x≈y → Eq.trans B (cong f x≈y) f≗g
@@ -91,8 +92,8 @@ CoreAdj = record
     open Functor Core      using () renaming (F₀ to Core₀; F₁ to Core₁)
     open Functor Forgetful using () renaming (F₀ to U₀   ; F₁ to U₁)
 
-    unit : ∀ S → S ⟶ Core₀ (U₀ S)
-    unit S = record { _⟨$⟩_ = Function.id ; cong = Function.id }
+    unit : ∀ S → Func S (Core₀ (U₀ S))
+    unit S = record { to = Function.id ; cong = Function.id }
 
     counit : ∀ A → PosetHomomorphism (U₀ (Core₀ A)) A
     counit A = mkPosetHomo (U₀ (Core₀ A)) A Function.id (reflexive A)
diff --git a/src/Categories/Adjoint/Mate.agda b/src/Categories/Adjoint/Mate.agda
index e2e725cb4..c70894499 100644
--- a/src/Categories/Adjoint/Mate.agda
+++ b/src/Categories/Adjoint/Mate.agda
@@ -6,7 +6,9 @@ module Categories.Adjoint.Mate where
 
 open import Level
 open import Data.Product using (Σ; _,_)
-open import Function.Equality using (Π; _⟶_; _⇨_) renaming (_∘_ to _∙_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Composition using (function)
+open import Function.Construct.Setoid using () renaming (function to _⇨_)
 open import Relation.Binary using (Setoid; IsEquivalence)
 
 open import Categories.Category
@@ -107,14 +109,32 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C}
 
   -- there are two squares to show
   module _ {X : C.Obj} {Y : D.Obj} where
-    open Setoid (L′⊣R′.Hom[L-,-].F₀ (X , Y) ⇨ L⊣R.Hom[-,R-].F₀ (X , Y))
+    private
+      From : Setoid _ _
+      From = L′⊣R′.Hom[L-,-].F₀ (X , Y)
+      To : Setoid _ _
+      To = L⊣R.Hom[-,R-].F₀ (X , Y)
+      SS = From ⇨ To
+    open Setoid SS using (_≈_)
     open C hiding (_≈_)
     open MR C
     open C.HomReasoning
     module DH = D.HomReasoning
-
-    mate-commute₁ : F₁ Hom[ C ][-,-] (C.id , β.η Y) ∙ L′⊣R′.Hom-inverse.to {X} {Y}
-                  ≈ L⊣R.Hom-inverse.to {X} {Y} ∙ F₁ Hom[ D ][-,-] (α.η X , D.id)
+    private
+      -- annoyingly the new bundles don't export this
+      D⟶C : Func (D.hom-setoid {F₀ L′ X} {Y}) (C.hom-setoid {X} {F₀ R′ Y})
+      D⟶C = record
+        { to = L′⊣R′.Hom-inverse.to {X} {Y}
+        ; cong = L′⊣R′.Hom-inverse.to-cong
+        }
+      D⟶C′ : Func D.hom-setoid C.hom-setoid
+      D⟶C′ = record
+        { to = L⊣R.Hom-inverse.to {X} {Y}
+        ; cong = L⊣R.Hom-inverse.to-cong
+        }
+
+    mate-commute₁ : function D⟶C (F₁ Hom[ C ][-,-] (C.id , β.η Y))
+                  ≈ function (F₁ Hom[ D ][-,-] (α.η X , D.id)) D⟶C′
     mate-commute₁ {f} {g} f≈g = begin
       β.η Y ∘ (F₁ R′ f ∘ L′⊣R′.unit.η X) ∘ C.id  ≈⟨ refl⟩∘⟨ identityʳ ⟩
       β.η Y ∘ F₁ R′ f ∘ L′⊣R′.unit.η X           ≈⟨ pullˡ (β.commute f) ⟩
@@ -124,14 +144,35 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C}
       F₁ R (D.id D.∘ g D.∘ α.η X) ∘ L⊣R.unit.η X ∎
 
   module _ {X : C.Obj} {Y : D.Obj} where
-    open Setoid (L′⊣R′.Hom[-,R-].F₀ (X , Y) ⇨ L⊣R.Hom[L-,-].F₀ (X , Y))
     open D hiding (_≈_)
     open MR D
     open D.HomReasoning
     module CH = C.HomReasoning
-
-    mate-commute₂ : F₁ Hom[ D ][-,-] (α.η X , D.id) ∙ L′⊣R′.Hom-inverse.from {X} {Y}
-                  ≈ L⊣R.Hom-inverse.from {X} {Y} ∙ F₁ Hom[ C ][-,-] (C.id , β.η Y)
+    private
+      From : Setoid _ _
+      From = L′⊣R′.Hom[-,R-].F₀ (X , Y)
+      To : Setoid _ _
+      To = L⊣R.Hom[L-,-].F₀ (X , Y)
+      module From = Setoid From
+      module To = Setoid To
+      SS : Setoid _ _
+      SS = From ⇨ To
+    open Setoid SS using (_≈_)
+    private
+      -- annoyingly the new bundles don't export this
+      C⟶D : Func C.hom-setoid D.hom-setoid
+      C⟶D = record
+        { to = L′⊣R′.Hom-inverse.from {X} {Y}
+        ; cong = L′⊣R′.Hom-inverse.from-cong
+        }
+      C⟶D′ : Func C.hom-setoid D.hom-setoid
+      C⟶D′ = record
+        { to = L⊣R.Hom-inverse.from {X} {Y}
+        ; cong = L⊣R.Hom-inverse.from-cong
+        }
+
+    mate-commute₂ : function C⟶D (F₁ Hom[ D ][-,-] (α.η X , D.id))
+                  ≈ function (F₁ Hom[ C ][-,-] (C.id , β.η Y)) C⟶D′
     mate-commute₂ {f} {g} f≈g = begin
       D.id ∘ (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X  ≈⟨ identityˡ ⟩
       (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X         ≈˘⟨ pushʳ (α.commute f) ⟩
diff --git a/src/Categories/Adjoint/Parametric.agda b/src/Categories/Adjoint/Parametric.agda
index b773d2853..d6a320f21 100644
--- a/src/Categories/Adjoint/Parametric.agda
+++ b/src/Categories/Adjoint/Parametric.agda
@@ -3,6 +3,9 @@ module Categories.Adjoint.Parametric where
 open import Level
 
 open import Data.Product using (_×_; _,_)
+open import Function.Bundles using (Injection; Inverse)
+open import Function.Properties.Inverse using (Inverse⇒Injection)
+
 open import Categories.Category.Core using (Category)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open Categories.Functor.Functor using (F₀; F₁; homomorphism; identity; F-resp-≈)
@@ -70,14 +73,14 @@ record ParametricAdjoint {C D E : Category o ℓ e} (L : Functor C (Functors D E
     ; F₁ = λ { {a , a'} {b , b'} (f , f') →
         η (L.₁ f') (RR.₀ b X) E.∘ LL.₁ a' (η (R.₁ f) X)}
     ; identity = λ { {a , a'} →
-        begin _ ≈⟨ L.identity ⟩∘⟨ Functor.F-resp-≈ (L.₀ a') R.identity ⟩
-              _ ≈⟨ refl⟩∘⟨ Functor.identity (L.₀ a') ⟩
+        begin _ ≈⟨ L.identity ⟩∘⟨ LL.F-resp-≈ a' R.identity ⟩
+              _ ≈⟨ refl⟩∘⟨ LL.identity a' ⟩
               _ ≈⟨ E.identity² ⟩
               _ ∎ }
     ; homomorphism = λ { {a , a'} {b , b'} →
         begin _ ≈⟨ pushˡ L.homomorphism ⟩
-              _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Functor.F-resp-≈ (L.₀ a') R.homomorphism ⟩
-              _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Functor.homomorphism (L.₀ a') ⟩
+              _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ LL.F-resp-≈ a' R.homomorphism ⟩
+              _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ LL.homomorphism a' ⟩
               _ ≈⟨ refl⟩∘⟨ pullˡ (commute (L.₁ _) _) ⟩
               _ ≈⟨ MR.assoc²'' E ⟩
               _ ∎ }
@@ -93,47 +96,49 @@ record ParametricAdjoint {C D E : Category o ℓ e} (L : Functor C (Functors D E
   counitCowedge {A} = record
     { E = A
     ; dinatural = dtHelper record
-      { α = λ c → A.counit.η c _
-      ; commute = λ {X} {Y} f →
-        let
-          open Adjoint
-
-          adjunction-isoˡ : A.Ladjunct X (A.counit.η X A E.∘ LL.₁ X (η (R.₁ f) A)) D.≈
-                            η (R.₁ f) A
-          adjunction-isoˡ = let open D.HomReasoning; open MR D in
-            begin _ ≈⟨ pushˡ (homomorphism (R.₀ X)) ⟩
-                  _ ≈⟨ pushʳ (D.Equiv.sym (A.unit.commute X _)) ⟩
-                  _ ≈⟨ A.zag X ⟩∘⟨refl ⟩
-                  _ ≈⟨ D.identityˡ ⟩
-                  _ ∎
-
-          adjunction-isoʳ : A.Ladjunct X (A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A)) D.≈
-                            η (R.₁ f) A
-          adjunction-isoʳ = let open D.HomReasoning; open MR D in
-            begin _ ≈⟨ pushˡ (homomorphism (R.₀ X)) ⟩
-                  _ ≈⟨ param-nat ⟩
-                  _ ≈⟨ refl⟩∘⟨ zag (areAdjoint Y) ⟩
-                  _ ≈⟨ refl⟩∘⟨ D.Equiv.sym (identity (R.₀ Y)) ⟩
-                  _ ≈⟨ refl⟩∘⟨ identity (R.₀ Y) ⟩
-                  _ ≈⟨ D.identityʳ ⟩
-                  _ ∎
-
-          adjunction-iso : A.Ladjunct X (A.Radjunct X (η (R.₁ f) A))
-                       D.≈ A.Ladjunct X (A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A))
-          adjunction-iso = D.Equiv.trans adjunction-isoˡ (D.Equiv.sym adjunction-isoʳ)
-
-          is-cowedge : A.Radjunct X (η (R.₁ f) A)
-                   E.≈ A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A)
-          is-cowedge = Adjoint.Hom-inverse.injective (areAdjoint X) adjunction-iso
-
-          -- in the proof the meat is in `is-cowedge`; but due to the definition of
-          -- cowedge using the constant bifunctor, Agda wants the proof term wrapped
-          -- in some identities.
-       in let open E.HomReasoning; open MR E in begin
-            _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ L.identity ⟩
-            _ ≈⟨ refl⟩∘⟨ is-cowedge ⟩
-            _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ introʳ (identity (L.₀ _)) ⟩
-            _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F-resp-≈ (L.₀ _) (D.Equiv.sym R.identity) ⟩
-            _ ∎
+      { α = λ c → A.counit.η c A
+      ; commute = λ {X} {Y} f → comm′ {X} {Y} f
       }
     }
+    where
+      open Adjoint
+      adjunction-isoˡ : ∀ {X Y} (f : X C.⇒ Y) → A.Ladjunct X (A.counit.η X A E.∘ LL.₁ X (η (R.₁ f) A)) D.≈ η (R.₁ f) A
+      adjunction-isoˡ {X} {Y} f = LRadjunct≈id (areAdjoint X)
+
+      -- note how the part inside the Ladjunct is not Radjunct
+      adjunction-isoʳ : ∀ {X Y} (f : X C.⇒ Y) → A.Ladjunct X (A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A)) D.≈ η (R.₁ f) A
+      adjunction-isoʳ {X} {Y} f = begin
+        A.Ladjunct X (A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A))                                      ≈⟨ D.Equiv.refl ⟩
+        F₁ (R.₀ X) (A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A)) D.∘ A.unit.η X (RR.₀ Y A)              ≈⟨ pushˡ (homomorphism (R.₀ X)) ⟩
+        F₁ (R.₀ X) (A.counit.η Y A) D.∘ F₁ (R.₀ X) (η (L.₁ f) (RR.₀ Y A)) D.∘ A.unit.η X (RR.₀ Y A) ≈⟨ param-nat ⟩
+        η (R.₁ f) _ D.∘ F₁ (R.₀ Y) (A.counit.η Y A) D.∘ A.unit.η Y (RR.₀ Y A)                       ≈⟨ (refl⟩∘⟨ zag (areAdjoint Y)) ⟩
+        η (R.₁ f) _ D.∘ D.id                                                                        ≈⟨ D.identityʳ ⟩
+        η (R.₁ f) A                                            ∎
+        where
+          open D.HomReasoning
+          open MR D
+      
+      adjunction-iso : ∀ {X Y} (f : X C.⇒ Y) → A.Ladjunct X (A.Radjunct X (η (R.₁ f) A))
+                       D.≈ A.Ladjunct X (A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A))
+      adjunction-iso {X} {Y} f = adjunction-isoˡ f ○ ⟺ (adjunction-isoʳ f)
+        where open D.HomReasoning
+
+      is-cowedge : ∀ {X Y} (f : X C.⇒ Y) → A.Radjunct X (η (R.₁ f) A) E.≈ A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A)
+      is-cowedge {X} {Y} f = Injection.injective (Inverse⇒Injection (Hom-inverse (areAdjoint X) (RR.₀ Y A) A)) (adjunction-iso f)
+      
+      -- the dinat needed is  DinaturalTransformation F (const E)
+      -- where F = PABifunctor {A} and E is A and G = const E
+      -- here we inline the definitions
+      comm′ : {X Y : C.Obj} (f : X C.⇒ Y) →
+         E.id {A} E.∘ A.counit.η X A E.∘ (F₁ (PABifunctor {A}) (f , C.id))
+           E.≈
+         E.id {A} E.∘ A.counit.η Y A E.∘ F₁ (PABifunctor {A}) (C.id , f)
+      comm′ {X} {Y} f = begin
+        E.id {A} E.∘ A.counit.η X A E.∘ (F₁ (PABifunctor {A}) (f , C.id))        ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ elimˡ L.identity) ⟩
+        E.id {A} E.∘ A.Radjunct X (η (R.₁ f) A)                                  ≈⟨ (refl⟩∘⟨ is-cowedge f) ⟩
+        E.id {A} E.∘ A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A)                     ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ introʳ (identity (L.₀ X))) ⟩
+        E.id {A} E.∘ A.counit.η Y A E.∘ η (L.₁ f) (RR.₀ Y A) E.∘ F₁ (L.₀ X) D.id ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ F-resp-≈ (L.₀ X) (D.Equiv.sym R.identity)) ⟩
+        E.id {A} E.∘ A.counit.η Y A E.∘ F₁ (PABifunctor {A}) (C.id , f)          ∎
+        where
+          open E.HomReasoning
+          open MR E
diff --git a/src/Categories/Adjoint/Relative.agda b/src/Categories/Adjoint/Relative.agda
index 43eb5e659..3036b4eeb 100644
--- a/src/Categories/Adjoint/Relative.agda
+++ b/src/Categories/Adjoint/Relative.agda
@@ -13,7 +13,7 @@ open import Level
 
 open import Data.Product using (_,_; _×_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality using (Π; _⟶_; _⟨$⟩_)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Relation.Binary using (Setoid)
 
 -- be explicit in imports to 'see' where the information comes from
@@ -69,7 +69,7 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record
   ; identityˡ = R.F-resp-≈ (iso.isoʳ _ D.Equiv.refl) ○ R.identity
   ; assoc = a
   ; sym-assoc = sym a
-  ; extend-≈ = λ k≈h → F-resp-≈ R (Π.cong (⇒.η _) k≈h)
+  ; extend-≈ = λ k≈h → F-resp-≈ R (Func.cong (⇒.η _) k≈h)
   }
   where
   open RelativeAdjoint RA
@@ -89,7 +89,7 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record
     R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id)               ≈⟨ introʳ J.identity ⟩
     (R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id)) ∘ J.₁ E.id  ≈⟨ assoc ⟩
     R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id) ∘ J.₁ E.id    ≈⟨ ⇐.sym-commute (E.id , ⇒.η (x , L.₀ y) ⟨$⟩ k) (D.Equiv.refl) ⟩
-    ⇐.η (x , L.₀ y) ⟨$⟩ ((⇒.η (x , L.₀ y) ⟨$⟩ k) D.∘ D.id D.∘ L.F₁ E.id)   ≈⟨ Π.cong (⇐.η _) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩
+    ⇐.η (x , L.₀ y) ⟨$⟩ ((⇒.η (x , L.₀ y) ⟨$⟩ k) D.∘ D.id D.∘ L.F₁ E.id)   ≈⟨ Func.cong (⇐.η _) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩
     ⇐.η (x , L.₀ y) ⟨$⟩ (⇒.η (x , L.₀ y) ⟨$⟩ k)                            ≈⟨ iso.isoˡ (x , _) Equiv.refl ⟩
     k            ∎
   a : {x y z : E.Obj} {k : J.₀ x ⇒ R.₀ (L.₀ y)} {l : J.₀ y ⇒ R.₀ (L.₀ z)} →
@@ -106,7 +106,7 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record
     module DR = D.HomReasoning
     lemma : ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ k D.≈ (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k)
     lemma = DR.begin
-      ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ k                DR.≈⟨ Π.cong (⇒.η xz) (refl⟩∘⟨ introʳ J.identity ) ⟩
+      ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ k                DR.≈⟨ Func.cong (⇒.η xz) (refl⟩∘⟨ introʳ J.identity ) ⟩
       ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ (k ∘ J.₁ E.id)   DR.≈⟨ ⇒.commute (E.id , ⇒.η yz ⟨$⟩ l) Equiv.refl ⟩
       (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k) D.∘ L.₁ E.id   DR.≈⟨ D.sym-assoc  ⟩
       ((⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k)) D.∘ L.₁ E.id DR.≈⟨ MR.elimʳ D L.identity ⟩
@@ -118,11 +118,11 @@ RA⇒RMonad {C = C} {D} {E} {J} RA = record
   ; R = R
   ; Hom-NI = record
     { F⇒G = ntHelper record
-      { η = λ _ → record { _⟨$⟩_ = Radjunct ; cong = ∘-resp-≈ʳ ∙ L.F-resp-≈ }
+      { η = λ _ → record { to = Radjunct ; cong = ∘-resp-≈ʳ ∙ L.F-resp-≈ }
       ; commute = λ _ x≈y → Radjunct-comm x≈y
       }
     ; F⇐G = ntHelper record
-      { η = λ _ → record { _⟨$⟩_ = Ladjunct ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈ }
+      { η = λ _ → record { to = Ladjunct ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈ }
       ; commute = λ _ x≈y → Ladjunct-comm x≈y
       }
     ; iso = λ X → record
diff --git a/src/Categories/Bicategory/Construction/Spans/Properties.agda b/src/Categories/Bicategory/Construction/Spans/Properties.agda
index bd73d1d92..5c66582d1 100644
--- a/src/Categories/Bicategory/Construction/Spans/Properties.agda
+++ b/src/Categories/Bicategory/Construction/Spans/Properties.agda
@@ -5,19 +5,18 @@ module Categories.Bicategory.Construction.Spans.Properties where
 open import Level
 
 open import Data.Product using (_,_; _×_)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as SR
-open import Function.Equality as SΠ renaming (id to ⟶-id)
 
-open import Categories.Category
-open import Categories.Category.Helper
-open import Categories.Category.Instance.Setoids
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical
+  using (pullback; FiberProduct)
 
-open import Categories.Diagram.Pullback
-
-open import Categories.Bicategory
-open import Categories.Bicategory.Monad
+open import Categories.Bicategory using (Bicategory)
+open import Categories.Bicategory.Monad using (Monad)
 
 import Categories.Category.Diagram.Span as Span
 import Categories.Bicategory.Construction.Spans as Spans
@@ -36,6 +35,7 @@ module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where
     open Bicategory Spans
 
     open Setoid renaming (_≈_ to [_][_≈_])
+    open Func
 
 
   -- We can view the roof of the span as a hom set! However, we need to partition
@@ -127,7 +127,7 @@ module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where
       ; sym = HomSetoid.sym
       ; trans = HomSetoid.trans
       }
-    ; ∘-resp-≈ = λ f≈h g≈i → cong (arr T.μ) (g≈i , f≈h)
+    ; ∘-resp-≈ = λ f≈h g≈i → Func.cong (arr T.μ) (g≈i , f≈h)
     }
       where
         open SR HomSetoid
diff --git a/src/Categories/Bicategory/Instance/EnrichedCats.agda b/src/Categories/Bicategory/Instance/EnrichedCats.agda
index 7439d3037..0c890cb7c 100644
--- a/src/Categories/Bicategory/Instance/EnrichedCats.agda
+++ b/src/Categories/Bicategory/Instance/EnrichedCats.agda
@@ -80,7 +80,7 @@ EnrichedCats = record
           open UnderlyingReasoning B
       in niHelper record
         { η       = λ {(_ , F) → from (NI.unitorˡ {C = A} {B} {F})}
-        ; η⁻¹     = λ {(lift tt , F) → to (NI.unitorˡ {C = A} {B} {F})}
+        ; η⁻¹     = λ {(lift _ , F) → to (NI.unitorˡ {C = A} {B} {F})}
         ; commute = λ { {_ , F} {_ , G} (_ , α) {X} →
           begin
             B.id ∘ (V.id V.∘ α [ X ]) ∘ B.id   ≈⟨ identityˡ ⟩
@@ -93,15 +93,15 @@ EnrichedCats = record
           module B = Underlying B
           open UnderlyingReasoning B
       in niHelper record
-        { η =  λ {(F , lift tt) → from (NI.unitorʳ {C = A} {B} {F}) }
+        { η =  λ {(F , lift _) → from (NI.unitorʳ {C = A} {B} {F}) }
         ; commute =  λ{ {_} {G , _} (α , _) {X} →
             begin
               B.id ∘ G $₁ A.id ∘ α [ X ]  ≈⟨ identityˡ ⟩
               G $₁ A.id ∘ α [ X ]         ≈⟨ UF.identity G ⟩∘⟨refl ⟩
               B.id ∘ α [ X ]              ≈⟨ id-comm-sym ⟩
               α [ X ] ∘ B.id              ∎ }
-        ; η⁻¹  = λ { (F , lift tt) → to (NI.unitorʳ {C = A} {B} {F}) }
-        ; iso  = λ { (F , lift tt) → iso (NI.unitorʳ {C = A} {B} {F}) }
+        ; η⁻¹  = λ { (F , lift _) → to (NI.unitorʳ {C = A} {B} {F}) }
+        ; iso  = λ { (F , lift _) → iso (NI.unitorʳ {C = A} {B} {F}) }
         }
     }
   ; triangle = λ {_ _ C f g X} → UnderlyingReasoning.identityʳ C
diff --git a/src/Categories/Category/Closed.agda b/src/Categories/Category/Closed.agda
index f1e9d14b3..55b181dcf 100644
--- a/src/Categories/Category/Closed.agda
+++ b/src/Categories/Category/Closed.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Categories.Category
+open import Categories.Category using (Category; module Commutation)
 
 module Categories.Category.Closed {o ℓ e} (C : Category o ℓ e) where
 
@@ -13,18 +13,19 @@ private
 
   open Commutation C
 
-open import Level
+open import Level using (Level; levelOfTerm)
 open import Data.Product using (Σ; _,_)
-open import Function.Equality using (_⟶_)
-open import Function.Inverse using (_InverseOf_; Inverse)
+open import Function.Bundles using (Func; Inverse)
+open import Function.Definitions using (Inverseᵇ)
 
-open import Categories.Category.Product
+open import Categories.Category.Product using (_⁂_)
 open import Categories.Functor renaming (id to idF)
-open import Categories.Functor.Bifunctor
-open import Categories.Functor.Construction.Constant
-open import Categories.NaturalTransformation
-open import Categories.NaturalTransformation.NaturalIsomorphism
+open import Categories.Functor.Bifunctor using (Bifunctor; appˡ; appʳ; flip-bifunctor)
+open import Categories.Functor.Construction.Constant using (const)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
 open import Categories.NaturalTransformation.Dinatural
+  using (Extranaturalʳ; extranaturalʳ; DinaturalTransformation)
 
 record Closed : Set (levelOfTerm C) where
   field
@@ -119,20 +120,23 @@ record Closed : Set (levelOfTerm C) where
                ⟩
 
   open Functor
+  open Func
 
-  γ : hom-setoid {X} {Y} ⟶ hom-setoid {unit} {[ X , Y ]₀}
+  γ : Func (hom-setoid {X} {Y}) (hom-setoid {unit} {[ X , Y ]₀})
   γ {X} = record
-    { _⟨$⟩_ = λ f → [ C.id , f ]₁ ∘ diagonal.α _
+    { to = λ f → [ C.id , f ]₁ ∘ diagonal.α _
     ; cong  = λ eq → ∘-resp-≈ˡ (F-resp-≈ [ X ,-] eq)
     }
 
   field
-    γ⁻¹             : hom-setoid {unit} {[ X , Y ]₀} ⟶ hom-setoid {X} {Y}
-    γ-inverseOf-γ⁻¹ : γ {X} {Y} InverseOf γ⁻¹
+    γ⁻¹            : Func (hom-setoid {unit} {[ X , Y ]₀}) (hom-setoid {X} {Y})
+    γ-γ⁻¹-inverseᵇ : Inverseᵇ _≈_ _≈_ (to γ⁻¹) (to (γ {X} {Y}))
 
   γ-inverse : Inverse (hom-setoid {unit} {[ X , Y ]₀}) (hom-setoid {X} {Y})
   γ-inverse = record
-    { to         = γ⁻¹
-    ; from       = γ
-    ; inverse-of = γ-inverseOf-γ⁻¹
+    { to        = to γ⁻¹
+    ; to-cong   = cong γ⁻¹
+    ; from      = to γ
+    ; from-cong = cong γ
+    ; inverse   = γ-γ⁻¹-inverseᵇ
     }
diff --git a/src/Categories/Category/Concrete/Properties.agda b/src/Categories/Category/Concrete/Properties.agda
index 5d305df6a..47b511099 100644
--- a/src/Categories/Category/Concrete/Properties.agda
+++ b/src/Categories/Category/Concrete/Properties.agda
@@ -2,16 +2,20 @@
 
 module Categories.Category.Concrete.Properties where
 
-open import Data.Unit.Polymorphic
-open import Function.Equality using (Π; _⟨$⟩_; const; _∘_)
-open import Level
+open import Data.Unit.Polymorphic using (⊤; tt)
+open import Function.Base using (const; _∘_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+import Function.Construct.Constant as Const
+import Function.Construct.Composition as Comp
+open import Level using (Level)
 open import Relation.Binary using (Setoid)
 import Relation.Binary.Reasoning.Setoid as SR
 
 open import Categories.Adjoint using (_⊣_; Adjoint)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Category.Concrete
+open import Categories.Category.Instance.SingletonSet using () renaming (SingletonSetoid to OneS)
+open import Categories.Category.Concrete using (Concrete; RepresentablyConcrete)
 open import Categories.Functor.Core using (Functor)
 open import Categories.Functor.Representable using (Representable)
 open import Categories.Functor.Properties using (Faithful)
@@ -19,6 +23,7 @@ import Categories.Morphism.Reasoning as MR
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 
 open Concrete
+open Func
 
 ⊣⇒Representable : {o ℓ e : Level} (C : Category o ℓ e) (conc : Concrete C ℓ e) → (F : Functor (Setoids ℓ e) C) →
   F ⊣ concretize conc  → RepresentablyConcrete C
@@ -29,20 +34,20 @@ open Concrete
     ; Iso = record
       { F⇒G = ntHelper record
         { η = λ X → record
-          { _⟨$⟩_ = λ x → L.counit.η X C.∘ F.₁ (const x)
+          { to = λ x → L.counit.η X C.∘ F.₁ (Const.function OneS (U.F₀ X) x)
           ; cong = λ i≈j → C.∘-resp-≈ʳ (F.F-resp-≈ λ _ → i≈j)
           }
         ; commute = λ {X} {Y} f {x} {y} x≈y →
             let open C.HomReasoning in begin
-            L.counit.η Y C.∘ F.₁ (const (U.₁ f ⟨$⟩ x))          ≈⟨ refl⟩∘⟨ F.F-resp-≈ (λ _ → Π.cong (U.₁ f) x≈y) ⟩
-            L.counit.η Y C.∘ F.₁ (U.F₁ f ∘ const y)            ≈⟨ pushʳ F.homomorphism ⟩
-            ((L.counit.η Y C.∘ F.₁ (U.₁ f)) C.∘ F.₁ (const y)) ≈⟨ pushˡ (commute L.counit f) ⟩
-            f C.∘ L.counit.η X C.∘ F.₁ (const y)               ≈˘⟨ C.identityʳ ⟩
-            (f C.∘ L.counit.η X C.∘ F.₁ (const y)) C.∘ C.id    ∎
+            L.counit.η Y C.∘ F.₁ (constF Y (U.₁ f ⟨$⟩ x))              ≈⟨ refl⟩∘⟨ F.F-resp-≈ (λ _ → cong (U.₁ f) x≈y) ⟩
+            L.counit.η Y C.∘ F.₁ (Comp.function (constF X y) (U.F₁ f)) ≈⟨ pushʳ F.homomorphism ⟩
+            ((L.counit.η Y C.∘ F.₁ (U.₁ f)) C.∘ F.₁ (constF X y))      ≈⟨ pushˡ (commute L.counit f) ⟩
+            f C.∘ L.counit.η X C.∘ F.₁ (constF X y)                    ≈˘⟨ C.identityʳ ⟩
+            (f C.∘ L.counit.η X C.∘ F.₁ (constF X y)) C.∘ C.id         ∎
         }
       ; F⇐G = ntHelper record
         { η = λ c → record
-          { _⟨$⟩_ = λ 1⇒c → U.₁ 1⇒c ⟨$⟩ η1
+          { to = λ 1⇒c → U.₁ 1⇒c ⟨$⟩ η1
           ; cong = λ i≈j → U.F-resp-≈ i≈j (Setoid.refl (U.₀ (F.₀ OneS)))
           }
         ; commute = λ {X} {Y} f {x} {y} x≈y →
@@ -54,11 +59,11 @@ open Concrete
              U.₁ f ⟨$⟩ (U.₁ y ⟨$⟩ η1)         ∎
         }
       ; iso = λ X → record
-        { isoˡ = λ {x} {y} x≈y → Setoid.trans (U.₀ X) (L.LRadjunct≈id {OneS} {X} {const x} tt) x≈y
+        { isoˡ = λ {x} {y} x≈y → Setoid.trans (U.₀ X) (L.LRadjunct≈id {OneS} {X} {Const.function OneS (U.F₀ X) x} tt) x≈y
         ; isoʳ = λ {1⇒x} {1⇒y} x≈y →
           let open C.HomReasoning in begin
-          L.counit.η X C.∘ F.₁ (const (U.₁ 1⇒x ⟨$⟩ η1))   ≈⟨ (refl⟩∘⟨ F.F-resp-≈ λ _ → U.F-resp-≈ x≈y Srefl) ⟩
-          L.counit.η X C.∘ F.₁ (U.₁ 1⇒y ∘ L.unit.η OneS)  ≈⟨ L.RLadjunct≈id {OneS} {X} {1⇒y}  ⟩
+          L.counit.η X C.∘ F.₁ (constF X (U.₁ 1⇒x ⟨$⟩ η1))                 ≈⟨ (refl⟩∘⟨ F.F-resp-≈ λ _ → U.F-resp-≈ x≈y Srefl) ⟩
+          L.counit.η X C.∘ F.₁ (Comp.function (L.unit.η OneS) (U.₁ 1⇒y))  ≈⟨ L.RLadjunct≈id {OneS} {X} {1⇒y}  ⟩
           1⇒y ∎
         }
       }
@@ -71,9 +76,8 @@ open Concrete
   module L = Adjoint L
   open NaturalTransformation
   open MR C
-  -- Is this somewhere else?  Should it be?
-  OneS : Setoid ℓ e
-  OneS = record { Carrier = ⊤ {ℓ} ; _≈_ = λ _ _ → ⊤ {e}}
   η1 : Setoid.Carrier (U.₀ (F.₀ OneS))
   η1 = L.unit.η OneS ⟨$⟩ tt
   Srefl = Setoid.refl (U.₀ (F.₀ OneS))
+  constF : ∀ {ℓ} A → Setoid.Carrier (U.F₀ A) → Func (OneS {ℓ}) (U.F₀ A)
+  constF A = Const.function OneS (U.F₀ A)
diff --git a/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda b/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda
index a34240c75..4157e325f 100644
--- a/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda
+++ b/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda
@@ -43,16 +43,10 @@ private
   module KaroubiEmbedding = Functor KaroubiEmbedding
 
 karoubi-embedding-full : Full KaroubiEmbedding
-karoubi-embedding-full = record
-  { from = record
-    { _⟨$⟩_ = λ f → BundledIdem.Idempotent⇒.hom f
-    ; cong = λ eq → eq
-    }
-  ; right-inverse-of = λ _ → refl
-  }
+karoubi-embedding-full f = BundledIdem.Idempotent⇒.hom f , refl
 
 karoubi-embedding-faithful : Faithful KaroubiEmbedding
-karoubi-embedding-faithful f g eq = eq
+karoubi-embedding-faithful eq = eq
 
 karoubi-embedding-fully-faithful : FullyFaithful KaroubiEmbedding
 karoubi-embedding-fully-faithful = karoubi-embedding-full , karoubi-embedding-faithful
diff --git a/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda b/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda
index 9b8954ebf..11194b8e5 100644
--- a/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda
+++ b/src/Categories/Category/Construction/Properties/Presheaves/Cartesian.agda
@@ -4,34 +4,31 @@ open import Categories.Category
 
 module Categories.Category.Construction.Properties.Presheaves.Cartesian {o ℓ e} (C : Category o ℓ e) where
 
-open import Level
-open import Data.Unit
+open import Level using (Level; _⊔_)
+open import Data.Unit.Polymorphic using (⊤)
 open import Data.Product using (_,_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent
-open import Function.Equality using (Π) renaming (_∘_ to _∙_)
-open import Relation.Binary
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Relation.Binary using (Setoid)
 
-open import Categories.Category.Cartesian
-open import Categories.Category.Construction.Presheaves
-open import Categories.Category.Instance.Setoids
-open import Categories.Functor
-open import Categories.Functor.Properties
-open import Categories.Functor.Presheaf
-open import Categories.NaturalTransformation
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Construction.Presheaves using (Presheaves′)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Functor.Presheaf using (Presheaf)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 
 import Categories.Object.Product as Prod
 import Categories.Morphism.Reasoning as MR
 
-open Π using (_⟨$⟩_)
-
 module _ {o′ ℓ′ o″ ℓ″} where
 
   Presheaves× : ∀ (A : Presheaf C (Setoids o′ ℓ′)) (A : Presheaf C (Setoids o″ ℓ″)) → Presheaf C (Setoids (o′ ⊔ o″) (ℓ′ ⊔ ℓ″))
   Presheaves× A B = record
     { F₀           = λ X → ×-setoid (A.₀ X) (B.₀ X)
     ; F₁           = λ f → record
-      { _⟨$⟩_ = λ { (a , b) → A.₁ f ⟨$⟩ a , B.₁ f ⟨$⟩ b }
-      ; cong  = λ { (eq₁ , eq₂) → Π.cong (A.₁ f) eq₁ , Π.cong (B.₁ f) eq₂ }
+      { to = λ { (a , b) → A.₁ f ⟨$⟩ a , B.₁ f ⟨$⟩ b }
+      ; cong  = λ { (eq₁ , eq₂) → Func.cong (A.₁ f) eq₁ , Func.cong (B.₁ f) eq₂ }
       }
     ; identity     = λ { (eq₁ , eq₂)    → A.identity eq₁ , B.identity eq₂ }
     ; homomorphism = λ { (eq₁ , eq₂)    → A.homomorphism eq₁ , B.homomorphism eq₂ }
@@ -48,14 +45,15 @@ module IsCartesian o′ ℓ′ where
     module P = Category P
     S = Setoids o′ ℓ′
     module S = Category S
+    open Func
 
   Presheaves-Cartesian : Cartesian P
   Presheaves-Cartesian = record
     { terminal = record
       { ⊤        = record
         { F₀           = λ x → record
-          { Carrier       = Lift o′ ⊤
-          ; _≈_           = λ _ _ → Lift ℓ′ ⊤
+          { Carrier       = ⊤
+          ; _≈_           = λ _ _ → ⊤
           ; isEquivalence = _
           }
         }
@@ -72,17 +70,17 @@ module IsCartesian o′ ℓ′ where
         { A×B      = Presheaves× A B
         ; π₁       = ntHelper record
           { η       = λ X → record
-            { _⟨$⟩_ = λ { (fst , _) → fst }
+            { to = λ { (fst , _) → fst }
             ; cong  = λ { (eq , _)  → eq }
             }
-          ; commute = λ { f (eq , _) → Π.cong (A.F₁ f) eq }
+          ; commute = λ { f (eq , _) → cong (A.F₁ f) eq }
           }
         ; π₂       = ntHelper record
           { η       = λ X → record
-            { _⟨$⟩_ = λ { (_ , snd) → snd }
+            { to = λ { (_ , snd) → snd }
             ; cong  = λ { (_ , eq)  → eq }
             }
-          ; commute = λ { f (_ , eq) → Π.cong (B.F₁ f) eq }
+          ; commute = λ { f (_ , eq) → cong (B.F₁ f) eq }
           }
         ; ⟨_,_⟩    = λ {F} α β →
           let module F = Functor F
@@ -90,26 +88,19 @@ module IsCartesian o′ ℓ′ where
               module β = NaturalTransformation β
           in ntHelper record
           { η       = λ Y → record
-            { _⟨$⟩_ = λ S → α.η Y ⟨$⟩ S , β.η Y ⟨$⟩ S
-            ; cong  = λ eq → Π.cong (α.η Y) eq , Π.cong (β.η Y) eq
+            { to = λ S → α.η Y ⟨$⟩ S , β.η Y ⟨$⟩ S
+            ; cong  = λ eq → cong (α.η Y) eq , cong (β.η Y) eq
             }
           ; commute = λ f eq → α.commute f eq , β.commute f eq
           }
         ; project₁ = λ {F α β x} eq →
-          let module F = Functor F
-              module α = NaturalTransformation α
-              module β = NaturalTransformation β
-          in Π.cong (α.η x) eq
+          let module α = NaturalTransformation α
+          in Func.cong (α.η x) eq
         ; project₂ = λ {F α β x} eq →
-          let module F = Functor F
-              module α = NaturalTransformation α
-              module β = NaturalTransformation β
-          in Π.cong (β.η x) eq
+          let module β = NaturalTransformation β
+          in cong (β.η x) eq
         ; unique   = λ {F α β δ} eq₁ eq₂ {x} eq →
           let module F = Functor F
-              module α = NaturalTransformation α
-              module β = NaturalTransformation β
-              module δ = NaturalTransformation δ
           in Setoid.sym (A.₀ x) (eq₁ (Setoid.sym (F.₀ x) eq))
            , Setoid.sym (B.₀ x) (eq₂ (Setoid.sym (F.₀ x) eq))
         }
diff --git a/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda b/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda
index 70483d271..798b220da 100644
--- a/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda
+++ b/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda
@@ -2,22 +2,21 @@
 
 module Categories.Category.Construction.Properties.Presheaves.CartesianClosed where
 
-open import Level
-open import Data.Unit
+open import Level using (Level; _⊔_)
+open import Data.Unit.Polymorphic using (⊤)
 open import Data.Product using (_,_; proj₁; proj₂)
-open import Function.Equality using (Π) renaming (_∘_ to _∙_)
-open import Relation.Binary
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Relation.Binary using (Setoid)
 
 open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.CartesianClosed using (CartesianClosed)
 open import Categories.Category.CartesianClosed.Canonical renaming (CartesianClosed to CCartesianClosed)
-open import Categories.Category.Construction.Presheaves
-open import Categories.Category.Instance.Setoids
-open import Categories.Functor using (Functor)
-open import Categories.Functor.Hom
-open import Categories.Functor.Properties
-open import Categories.Functor.Presheaf
+open import Categories.Category.Construction.Presheaves using (Presheaves; Presheaves′)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Functor.Hom using (Hom[_][_,_]; Hom[_][-,_])
+open import Categories.Functor.Presheaf using (Presheaf)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Categories.Object.Terminal using (Terminal)
 
@@ -25,7 +24,7 @@ import Categories.Category.Construction.Properties.Presheaves.Cartesian as Pre
 import Categories.Morphism.Reasoning as MR
 import Relation.Binary.Reasoning.Setoid as SetoidR
 
-open Π using (_⟨$⟩_)
+open Func
 
 module HasClosed {o ℓ e} (C : Category o ℓ e) where
   private
@@ -43,17 +42,17 @@ module HasClosed {o ℓ e} (C : Category o ℓ e) where
     Presheaf^ = record
       { F₀           = λ X → Hom[ Presheaves C ][ Presheaves× Hom[ C ][-, X ] G , F ]
       ; F₁           = λ {A B} f → record
-        { _⟨$⟩_ = λ α →
+        { to = λ α →
           let module α = NaturalTransformation α using (η; commute)
           in ntHelper record
           { η       = λ X → record
-            { _⟨$⟩_ = λ where (g , S) → α.η X ⟨$⟩ (f ∘ g , S)
-            ; cong  = λ where (eq₁ , eq₂) → Π.cong (α.η X) (∘-resp-≈ʳ eq₁ , eq₂)
+            { to = λ where (g , S) → α.η X ⟨$⟩ (f ∘ g , S)
+            ; cong  = λ where (eq₁ , eq₂) → cong (α.η X) (∘-resp-≈ʳ eq₁ , eq₂)
             }
           ; commute = λ { {Z} {W} g {h , x} {i , y} (eq₁ , eq₂) →
             let open SetoidR (F.₀ W)
             in begin
-              α.η W ⟨$⟩ (f ∘ C.id ∘ h ∘ g , G.₁ g ⟨$⟩ x)   ≈⟨ Π.cong (α.η W) (Equiv.trans (pullˡ id-comm) (center Equiv.refl) , Setoid.refl (G.₀ W)) ⟩
+              α.η W ⟨$⟩ (f ∘ C.id ∘ h ∘ g , G.₁ g ⟨$⟩ x)   ≈⟨ cong (α.η W) (Equiv.trans (pullˡ id-comm) (center Equiv.refl) , Setoid.refl (G.₀ W)) ⟩
               α.η W ⟨$⟩ (C.id ∘ (f ∘ h) ∘ g , G.₁ g ⟨$⟩ x) ≈⟨ α.commute g (∘-resp-≈ʳ eq₁ , eq₂) ⟩
               F.₁ g ⟨$⟩ (α.η Z ⟨$⟩ (f ∘ i , y))            ∎ }
           }
@@ -90,7 +89,7 @@ module IsCartesianClosed {o} (C : Category o o o) where
           module G = Functor G
       in ntHelper record
       { η       = λ X → record
-        { _⟨$⟩_ = λ { (α , x) →
+        { to = λ { (α , x) →
           let module α = NaturalTransformation α
           in α.η X ⟨$⟩ (C.id , x) }
         ; cong  = λ where (eq₁ , eq₂) → eq₁ (C.Equiv.refl , eq₂)
@@ -111,25 +110,25 @@ module IsCartesianClosed {o} (C : Category o o o) where
           module α = NaturalTransformation α
       in ntHelper record
       { η       = λ X → record
-        { _⟨$⟩_ = λ x → ntHelper record
+        { to = λ x → ntHelper record
           { η       = λ Y → record
-            { _⟨$⟩_ = λ where (f , y) → α.η Y ⟨$⟩ (F.₁ f ⟨$⟩ x , y)
-            ; cong  = λ where (eq₁ , eq₂) → Π.cong (α.η _) (F.F-resp-≈ eq₁ (Setoid.refl (F.₀ _)) , eq₂)
+            { to = λ where (f , y) → α.η Y ⟨$⟩ (F.₁ f ⟨$⟩ x , y)
+            ; cong  = λ where (eq₁ , eq₂) → cong (α.η _) (F.F-resp-≈ eq₁ (Setoid.refl (F.₀ _)) , eq₂)
             }
           ; commute = λ { {Y} {Z} f {g , y} {h , z} (eq₁ , eq₂) →
             let open SetoidR (H.₀ Z)
                 open Setoid  (G.₀ Z)
             in begin
               α.η Z ⟨$⟩ (F.F₁ (C.id C.∘ g C.∘ f) ⟨$⟩ x , G.F₁ f ⟨$⟩ y)
-                ≈⟨ Π.cong (α.η Z) (F.F-resp-≈ C.identityˡ (Setoid.refl (F.₀ X)) , refl) ⟩
+                ≈⟨ cong (α.η Z) (F.F-resp-≈ C.identityˡ (Setoid.refl (F.₀ X)) , refl) ⟩
               α.η Z ⟨$⟩ (F.F₁ (g C.∘ f) ⟨$⟩ x , G.F₁ f ⟨$⟩ y)
-                ≈⟨ Π.cong (α.η Z) (F.homomorphism (Setoid.refl (F.₀ X)) , refl) ⟩
+                ≈⟨ cong (α.η Z) (F.homomorphism (Setoid.refl (F.₀ X)) , refl) ⟩
               α.η Z ⟨$⟩ (F.F₁ f ⟨$⟩ (F.F₁ g ⟨$⟩ x) , G.F₁ f ⟨$⟩ y)
                 ≈⟨ α.commute f (F.F-resp-≈ eq₁ (Setoid.refl (F.₀ X)) , eq₂) ⟩
               H.F₁ f ⟨$⟩ (α.η Y ⟨$⟩ (F.F₁ h ⟨$⟩ x , z))
                 ∎ }
           }
-          ; cong  = λ where eq (eq₁ , eq₂) → Π.cong (α.η _) (F.F-resp-≈ eq₁ eq , eq₂)
+          ; cong  = λ where eq (eq₁ , eq₂) → cong (α.η _) (F.F-resp-≈ eq₁ eq , eq₂)
         }
       ; commute = λ { {X} {Y} f {x} {y} eq {Z} {g , z} {h , w} (eq₁ , eq₂) →
         let open SetoidR (F.₀ Z)
@@ -139,12 +138,12 @@ module IsCartesianClosed {o} (C : Category o o o) where
               F.₁ g ⟨$⟩ (F.₁ f ⟨$⟩ x) ≈⟨ F.F-resp-≈ eq (Setoid.refl (F.₀ Y)) ⟩
               F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ x) ≈˘⟨ F.homomorphism (Setoid.sym (F.₀ X) eq′) ⟩
               F.₁ (f C.∘ h) ⟨$⟩ y     ∎
-        in Π.cong (α.η _) (helper eq₁ eq , eq₂) }
+        in cong (α.η _) (helper eq₁ eq , eq₂) }
       }
     ; eval-comp    = λ {F G H} {α} → λ { (eq₁ , eq₂) →
       let module H  = Functor H
           module α  = NaturalTransformation α
-      in Π.cong (α.η _) (H.identity eq₁ , eq₂) }
+      in cong (α.η _) (H.identity eq₁ , eq₂) }
     ; curry-unique = λ {F G H} {α β} eq {X} {x y} eq₁ → λ { {Y} {f , z} {g , w} (eq₂ , eq₃) →
       let module F = Functor F
           module G = Functor G
@@ -156,7 +155,7 @@ module IsCartesianClosed {o} (C : Category o o o) where
           open SetoidR (G.₀ Y)
       in begin
         αXx.η Y ⟨$⟩ (f , z)
-          ≈⟨ Π.cong (αXx.η _) (C.Equiv.sym C.identityʳ , refl) ⟩
+          ≈⟨ cong (αXx.η _) (C.Equiv.sym C.identityʳ , refl) ⟩
         αXx.η Y ⟨$⟩ (f C.∘ C.id , z)
           ≈⟨ α.sym-commute f (Setoid.refl (F.₀ X)) (C.Equiv.refl , refl) ⟩
         NaturalTransformation.η (α.η Y ⟨$⟩ (F.F₁ f ⟨$⟩ x)) Y ⟨$⟩ (C.id , z)
diff --git a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
index 6bcf01daa..7bbf189c1 100644
--- a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
+++ b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
@@ -2,24 +2,25 @@
 
 module Categories.Category.Construction.Properties.Presheaves.FromCartesianCCC where
 
-open import Level
-open import Data.Unit
+open import Level using (Level; _⊔_)
 open import Data.Product using (_,_; proj₁; proj₂)
-open import Function.Equality using (Π) renaming (_∘_ to _∙_)
-open import Relation.Binary
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Composition using (function)
+open import Function.Construct.Setoid using (_∙_)
+open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidR
 
-open import Categories.Category.BinaryProducts
+open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.CartesianClosed using (CartesianClosed)
 open import Categories.Category.CartesianClosed.Canonical renaming (CartesianClosed to CCartesianClosed)
-open import Categories.Category.Construction.Presheaves
-open import Categories.Category.Instance.Setoids
-open import Categories.Functor
-open import Categories.Functor.Hom
-open import Categories.Functor.Properties
-open import Categories.Functor.Presheaf
+open import Categories.Category.Construction.Presheaves using (Presheaves′; Presheaves)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Functor.Hom using (Hom[_][_,_])
+open import Categories.Functor.Properties using ([_]-resp-∘; [_]-resp-square)
+open import Categories.Functor.Presheaf using (Presheaf)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Categories.Object.Terminal using (Terminal)
 
@@ -27,8 +28,6 @@ import Categories.Category.Construction.Properties.Presheaves.Cartesian as Pre
 import Categories.Object.Product as Prod
 import Categories.Morphism.Reasoning as MR
 
-open Π using (_⟨$⟩_)
-
 module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesian C) where
   private
     module C = Category C
@@ -62,9 +61,9 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi
   ExpF : (F : Presheaf C (Setoids o′ ℓ′)) → Functor C.op P
   ExpF F = record
     { F₀           = Pres-exp F
-    ; F₁           = λ {A B} f → ntHelper record
+    ; F₁           = λ f → ntHelper record
       { η       = λ X → F₁ (first f)
-      ; commute = λ {X Y} g {x y} eq →
+      ; commute = λ g eq →
         [ F ]-resp-square (C.Equiv.sym first↔second) eq
       }
     ; identity     = λ {A B} {x y} eq →
@@ -93,18 +92,18 @@ module FromCartesian o′ ℓ′ {o ℓ e} {C : Category o ℓ e} (Car : Cartesi
     Presheaf^ = record
       { F₀           = λ X → Hom[ Presheaves C ][ G , Pres-exp F X ]
       ; F₁           = λ {A B} f → record
-        { _⟨$⟩_ = λ α →
+        { to = λ α →
           let module α = NaturalTransformation α
           in ntHelper record
           { η       = λ X → F.₁ (first f) ∙ α.η X
           ; commute = λ {X Y} g  {x y} eq →
             let open SetoidR (F.₀ (B × Y))
             in begin
-              F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ g ⟨$⟩ x))          ≈⟨ Π.cong (F.₁ (first f)) (α.commute g eq) ⟩
+              F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ g ⟨$⟩ x))          ≈⟨ Func.cong (F.₁ (first f)) (α.commute g eq) ⟩
               F.₁ (first f) ⟨$⟩ (F.₁ (second g) ⟨$⟩ (α.η X ⟨$⟩ y)) ≈˘⟨ [ F ]-resp-square first↔second (Setoid.refl (F.₀ (A × X))) ⟩
               F.₁ (second g) ⟨$⟩ (F.₁ (first f) ⟨$⟩ (α.η X ⟨$⟩ y)) ∎
           }
-        ; cong  = λ eq eq′ → Π.cong (F.₁ (first f)) (eq eq′)
+        ; cong  = λ eq eq′ → Func.cong (F.₁ (first f)) (eq eq′)
         }
       ; identity     = λ {X} {α β} eq {Y} {x y} eq′ →
         let module α = NaturalTransformation α
@@ -125,13 +124,12 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
     module C  = Category C using (identityˡ; id; module HomReasoning)
     module CH = C.HomReasoning
     P = Presheaves′ o o C
-    -- open Cartesian Car
     open BinaryProducts (Cartesian.products Car) using (_×_; π₁; π₂; ⟨_,_⟩; Δ; first; second; _⁂_; Δ∘; ⁂∘Δ; second∘first;
       π₁∘⁂; π₂∘⁂; project₁; project₂; η)
-    -- module CarP = BinaryProducts products
     open Preₚ.IsCartesian C o o using () renaming (Presheaves-Cartesian to PC)
     module PPC = BinaryProducts PC.products using (π₁; π₂; _×_; project₁; project₂; ⟨_,_⟩; unique)
     module TPC = Terminal PC.terminal using (⊤; !; !-unique)
+    open Func
 
   CanonicalCCC : CCartesianClosed P
   CanonicalCCC = record
@@ -151,10 +149,10 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
           module G = Functor G using (₀; ₁)
       in ntHelper record
         { η       = λ X → record
-          { _⟨$⟩_ = λ { (α , x) →
+          { to = λ { (α , x) →
             let module α = NaturalTransformation α using (η)
             in F.₁ Δ ⟨$⟩ (α.η X ⟨$⟩ x) }
-          ; cong  = λ { (eq , eq′) → Π.cong (F.₁ Δ) (eq eq′) }
+          ; cong  = λ { (eq , eq′) → cong (F.₁ Δ) (eq eq′) }
           }
         ; commute = λ {X Y} f → λ { {α , x} {β , y} (eq , eq′) →
           let module α = NaturalTransformation α using (η; commute)
@@ -162,8 +160,8 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
               open Setoid  (F.₀ (X × X)) using (sym; refl)
               open SetoidR (F.₀ Y)
           in  begin
-            F.₁ Δ ⟨$⟩ (F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ f ⟨$⟩ x)))    ≈⟨ Π.cong (F.₁ Δ ∙ F.₁ (first f)) (α.commute f eq′) ⟩
-            F.₁ Δ ∙ F.₁ (first f) ∙ F.₁ (second f) ⟨$⟩ (α.η X ⟨$⟩ y) ≈⟨ Π.cong (F.₁ Δ) ([ F ]-resp-∘ second∘first refl) ⟩
+            F.₁ Δ ⟨$⟩ (F.₁ (first f) ⟨$⟩ (α.η Y ⟨$⟩ (G.₁ f ⟨$⟩ x)))    ≈⟨ cong (F.₁ Δ ∙ F.₁ (first f)) (α.commute f eq′) ⟩
+            F.₁ Δ ∙ (F.₁ (first f) ∙ F.₁ (second f)) ⟨$⟩ (α.η X ⟨$⟩ y) ≈⟨ cong (F.₁ Δ) ([ F ]-resp-∘ second∘first refl) ⟩
             F.₁ Δ ⟨$⟩ (F.₁ (f ⁂ f) ⟨$⟩ (α.η X ⟨$⟩ y))                 ≈⟨ [ F ]-resp-∘ ⁂∘Δ refl ⟩
             F.₁ ⟨ f , f ⟩ ⟨$⟩ (α.η X ⟨$⟩ y)                           ≈˘⟨ [ F ]-resp-∘ Δ∘ (sym (eq (Setoid.refl (G.₀ X)))) ⟩
             F.₁ f ⟨$⟩ (F.₁ Δ ⟨$⟩ (β.η X ⟨$⟩ y))
@@ -176,32 +174,32 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
           module α = NaturalTransformation α
       in ntHelper record
         { η       = λ X → record
-          { _⟨$⟩_ = λ x → ntHelper record
+          { to = λ x → ntHelper record
             { η       = λ Y → record
-              { _⟨$⟩_ = λ y → α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ y)
-              ; cong  = λ eq → Π.cong (α.η (X × Y)) (Setoid.refl (F.₀ (X × Y)) , Π.cong (G.₁ π₂) eq)
+              { to = λ y → α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ y)
+              ; cong  = λ eq → cong (α.η (X × Y)) (Setoid.refl (F.₀ (X × Y)) , cong (G.₁ π₂) eq)
               }
             ; commute = λ {Y Z} f {y z} eq →
               let open SetoidR (H.₀ (X × Z))
               in begin
                 α.η (X × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ (G.₁ f ⟨$⟩ y))
-                  ≈˘⟨ Π.cong (α.η (X × Z)) ( [ F ]-resp-∘ (π₁∘⁂ CH.○ C.identityˡ) (Setoid.refl (F.₀ X))
+                  ≈˘⟨ cong (α.η (X × Z)) ( [ F ]-resp-∘ (π₁∘⁂ CH.○ C.identityˡ) (Setoid.refl (F.₀ X))
                                            , [ G ]-resp-square π₂∘⁂ (Setoid.refl (G.₀ Y))) ⟩
                 α.η (X × Z) ⟨$⟩ (F.₁ (second f) ∙ F.₁ π₁ ⟨$⟩ x , G.₁ (second f) ⟨$⟩ (G.₁ π₂ ⟨$⟩ y))
-                  ≈⟨ α.commute (second f) (Setoid.refl (F.₀ (X × Y)) , Π.cong (G.₁ π₂) eq) ⟩
+                  ≈⟨ α.commute (second f) (Setoid.refl (F.₀ (X × Y)) , cong (G.₁ π₂) eq) ⟩
                 H.₁ (second f) ⟨$⟩ (α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ z))
                   ∎
             }
-          ; cong  = λ eq₁ eq₂ → Π.cong (α.η _) (Π.cong (F.F₁ π₁) eq₁ , Π.cong (G.₁ π₂) eq₂)
+          ; cong  = λ eq₁ eq₂ → cong (α.η _) (cong (F.F₁ π₁) eq₁ , cong (G.₁ π₂) eq₂)
           }
         ; commute = λ {X Y} f {x y} eq₁ {Z} {z w} eq₂ →
           let open SetoidR (H.₀ (Y × Z))
           in begin
             α.η (Y × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ (F.₁ f ⟨$⟩ x) , G.₁ π₂ ⟨$⟩ z)
-              ≈˘⟨ Π.cong (α.η _) ( [ F ]-resp-square π₁∘⁂ (Setoid.refl (F.₀ X))
+              ≈˘⟨ cong (α.η _) ( [ F ]-resp-square π₁∘⁂ (Setoid.refl (F.₀ X))
                                  , [ G ]-resp-∘ (π₂∘⁂ CH.○ C.identityˡ) (Setoid.refl (G.₀ Z))) ⟩
             α.η (Y × Z) ⟨$⟩ (F.₁ (first f) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x) , G.₁ (first f) ⟨$⟩ (G.₁ π₂ ⟨$⟩ z))
-              ≈⟨ α.commute (first f) (Π.cong (F.₁ π₁) eq₁ , Π.cong (G.₁ π₂) eq₂) ⟩
+              ≈⟨ α.commute (first f) (cong (F.₁ π₁) eq₁ , cong (G.₁ π₂) eq₂) ⟩
             H.₁ (first f) ⟨$⟩ (α.η (X × Z) ⟨$⟩ (F.₁ π₁ ⟨$⟩ y , G.₁ π₂ ⟨$⟩ w))
               ∎
         }
@@ -215,11 +213,11 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
           open SetoidR (F.₀ X)
       in begin
         F.₁ Δ ⟨$⟩ (α.η (X × X) ⟨$⟩ (H.₁ π₁ ⟨$⟩ x , G.₁ π₂ ⟨$⟩ y))
-          ≈⟨ α.sym-commute Δ (Π.cong (H.₁ π₁) eq₁ , Π.cong (G.₁ π₂) eq₂) ⟩
+          ≈⟨ α.sym-commute Δ (cong (H.₁ π₁) eq₁ , cong (G.₁ π₂) eq₂) ⟩
         α.η X ⟨$⟩ (H.₁ Δ ⟨$⟩ (H.F₁ π₁ ⟨$⟩ z) , G.₁ Δ ⟨$⟩ (G.₁ π₂ ⟨$⟩ w))
-          ≈⟨ Π.cong (α.η X) ([ H ]-resp-∘ project₁ HX.refl , [ G ]-resp-∘ project₂ GX.refl) ⟩
+          ≈⟨ cong (α.η X) ([ H ]-resp-∘ project₁ HX.refl , [ G ]-resp-∘ project₂ GX.refl) ⟩
         α.η X ⟨$⟩ (H.F₁ C.id ⟨$⟩ z , G.F₁ C.id ⟨$⟩ w)
-          ≈⟨ Π.cong (α.η X) (H.identity HX.refl , G.identity GX.refl) ⟩
+          ≈⟨ cong (α.η X) (H.identity HX.refl , G.identity GX.refl) ⟩
         α.η X ⟨$⟩ (z , w)
           ∎ }
     ; curry-unique = λ {F G H} {α β} eq {X} {x y} eq₁ {Y} {z w} eq₂ →
@@ -237,13 +235,13 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
         G.₁ C.id ⟨$⟩ (αXx.η Y ⟨$⟩ z)
           ≈˘⟨ [ G ]-resp-∘ (⁂∘Δ CH.○ η) GXY.refl ⟩
         G.₁ Δ ⟨$⟩ (G.F₁ (π₁ ⁂ π₂) ⟨$⟩ (αXx.η Y ⟨$⟩ z))
-          ≈˘⟨ Π.cong (G.₁ Δ) ([ G ]-resp-∘ second∘first GXY.refl) ⟩
+          ≈˘⟨ cong (G.₁ Δ) ([ G ]-resp-∘ second∘first GXY.refl) ⟩
         G.₁ Δ ⟨$⟩ (G.₁ (first π₁) ⟨$⟩ (G.₁ (second π₂) ⟨$⟩ (αXx.η Y ⟨$⟩ z)))
-          ≈⟨ Π.cong (G.₁ Δ ∙ G.₁ (first π₁)) (αXx.sym-commute π₂ (Setoid.refl (H.₀ Y))) ⟩
+          ≈⟨ cong (G.₁ Δ ∙ G.₁ (first π₁)) (αXx.sym-commute π₂ (Setoid.refl (H.₀ Y))) ⟩
         G.₁ Δ ⟨$⟩ (G.₁ (first π₁) ⟨$⟩ (αXx.η (X × Y) ⟨$⟩ (H.₁ π₂ ⟨$⟩ z)))
-          ≈⟨ Π.cong (G.₁ Δ) (α.sym-commute π₁ (Setoid.refl (F.₀ X)) (Setoid.refl (H.₀ (X × Y)))) ⟩
+          ≈⟨ cong (G.₁ Δ) (α.sym-commute π₁ (Setoid.refl (F.₀ X)) (Setoid.refl (H.₀ (X × Y)))) ⟩
         G.₁ Δ ⟨$⟩ (NaturalTransformation.η (α.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ x)) (X × Y) ⟨$⟩ (H.₁ π₂ ⟨$⟩ z))
-          ≈⟨ eq (Π.cong (F.₁ π₁) eq₁ , Π.cong (H.₁ π₂) eq₂) ⟩
+          ≈⟨ eq (cong (F.₁ π₁) eq₁ , cong (H.₁ π₂) eq₂) ⟩
         β.η (X × Y) ⟨$⟩ (F.₁ π₁ ⟨$⟩ y , H.₁ π₂ ⟨$⟩ w)
           ∎
     }
diff --git a/src/Categories/Category/Instance/EmptySet.agda b/src/Categories/Category/Instance/EmptySet.agda
index 021f0ae6f..dd313c5b8 100644
--- a/src/Categories/Category/Instance/EmptySet.agda
+++ b/src/Categories/Category/Instance/EmptySet.agda
@@ -8,8 +8,6 @@ module Categories.Category.Instance.EmptySet where
 
 open import Data.Unit
 open import Data.Empty using (⊥; ⊥-elim)
-open import Function.Equality using (Π)
-open Π using (_⟨$⟩_)
 
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality using (refl)
@@ -38,7 +36,7 @@ module _ {c ℓ : Level} where
     { ⊥            = EmptySetoid
     ; ⊥-is-initial = record
       { !        = record
-        { _⟨$⟩_ = λ { () }
+        { to = λ { () }
         ; cong  = λ { {()} }
         }
       ; !-unique = λ { _ {()} }
diff --git a/src/Categories/Category/Instance/FamilyOfSetoids.agda b/src/Categories/Category/Instance/FamilyOfSetoids.agda
index cdd98317c..fd0a41dc6 100644
--- a/src/Categories/Category/Instance/FamilyOfSetoids.agda
+++ b/src/Categories/Category/Instance/FamilyOfSetoids.agda
@@ -7,17 +7,22 @@ module Categories.Category.Instance.FamilyOfSetoids where
 -- This particular formalization should be considered alpha, i.e. its
 -- names will change once things settle.
 
-open import Level
+open import Level using (Level; _⊔_; suc)
+open import Function.Base renaming (id to idf; _∘_ to _⊚_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to idF)
+open import Function.Construct.Composition using (function)
+open import Function.Construct.Setoid using (_∙_) renaming (function to _⇨_)
+open import Function.Structures using (IsInverse)
 open import Relation.Binary
   using (Rel; Setoid; module Setoid; Reflexive; Symmetric; Transitive)
-open import Function.Base renaming (id to idf; _∘_ to _⊚_)
-open import Function.Equality
-open import Function.Inverse using (_InverseOf_)
 import Relation.Binary.Reasoning.Setoid as SetoidR
 
-open import Categories.Category
+open import Categories.Category.Core using (Category)
+open Func
 
 module _ {a b c d : Level} where
+
   record Fam : Set (suc (a ⊔ b ⊔ c ⊔ d)) where
     constructor fam
     open Setoid using () renaming (Carrier to ∣_∣; _≈_ to _≈≈_)
@@ -26,14 +31,14 @@ module _ {a b c d : Level} where
     open Setoid U hiding (Carrier)
     field
       T : ∣ U ∣ → Setoid c d
-      reindex : {x y : ∣ U ∣} (P : x ≈ y) → T y ⟶ T x
+      reindex : {x y : ∣ U ∣} (P : x ≈ y) → Func (T y) (T x)
 
       -- the following coherence laws are needed to make _≃_ below an equivalence
       reindex-refl : {x : ∣ U ∣} {bx : ∣ T x ∣} → _≈≈_ (T x) (reindex refl ⟨$⟩ bx) bx
-      reindex-sym : {x y : ∣ U ∣} → (p : x ≈ y) → (reindex (sym p)) InverseOf (reindex p)
+      reindex-sym : {x y : ∣ U ∣} → (p : x ≈ y) → IsInverse (_≈≈_ (T x)) (_≈≈_ (T y)) (to (reindex (sym p))) (to (reindex p))
       reindex-trans : {x y z : ∣ U ∣} {b : ∣ T z ∣} → (p : x ≈ y) → (q : y ≈ z) →
         Setoid._≈_ (T x) (reindex (trans p q) ⟨$⟩ b)
-                         (reindex p ∘ reindex q ⟨$⟩ b)
+                         (reindex p ∙ reindex q ⟨$⟩ b)
   open Fam
 
 
@@ -41,12 +46,12 @@ module _ {a b c d : Level} where
     constructor fhom
     open Setoid (U B) using (_≈_)
     field
-      map : U B ⟶ U B′
-      transport : (x : Setoid.Carrier (U B)) → T B x ⟶ T B′ (map ⟨$⟩ x)
+      map : Func (U B) (U B′)
+      transport : (x : Setoid.Carrier (U B)) → Func (T B x) (T B′ (map ⟨$⟩ x))
       transport-coh : {x y : Setoid.Carrier (U B)} → (p : x ≈ y) →
         Setoid._≈_ (T B y ⇨ T B′ (map ⟨$⟩ x))
-          (transport x ∘ reindex B p)
-          (reindex B′ (Π.cong map p) ∘ transport y)
+          (transport x ∙ reindex B p)
+          (reindex B′ (cong map p) ∙ transport y)
 
   record _≈≈_ {X Y} (F F′ : (Hom X Y)) : Set (a ⊔ b ⊔ c ⊔ d) where
     constructor feq
@@ -58,17 +63,17 @@ module _ {a b c d : Level} where
       g≈f : {x : A} → map F ⟨$⟩ x ≈ map F′ ⟨$⟩ x
       φ≈γ : {x : A} → let C = T X x
                           D = T Y (map F ⟨$⟩ x) in
-            {bx : Setoid.Carrier C} → Setoid._≈_ D ((reindex Y g≈f ∘ transport F′ x) ⟨$⟩ bx) (transport F x ⟨$⟩ bx)
+            {bx : Setoid.Carrier C} → Setoid._≈_ D ((reindex Y g≈f ∙ transport F′ x) ⟨$⟩ bx) (transport F x ⟨$⟩ bx)
 
   fam-id : {A : Fam} → Hom A A
-  fam-id {A} = fhom id (λ _ → id) λ p x≈y → Π.cong (reindex A p) x≈y
+  fam-id {A} = fhom (idF (U A)) (λ x → idF (T A x)) λ p x≈y → cong (reindex A p) x≈y
   comp : {A B C : Fam} → Hom B C → Hom A B → Hom A C
   comp {B = B} {C} (fhom map₀ trans₀ coh₀) (fhom map₁ trans₁ coh₁) =
-    fhom (map₀ ∘ map₁) (λ x → trans₀ (map₁ ⟨$⟩ x) ∘ (trans₁ x))
+    fhom (map₀ ∙ map₁) (λ x → trans₀ (map₁ ⟨$⟩ x) ∙ (trans₁ x))
          λ {a} {b} p {x} {y} x≈y →
-           let open Setoid (T C (map₀ ∘ map₁ ⟨$⟩ a)) renaming (trans to _⟨≈⟩_) in
-           Π.cong (trans₀ (map₁ ⟨$⟩ a)) (coh₁ p x≈y) ⟨≈⟩
-           coh₀ (Π.cong map₁ p) (Setoid.refl (T B (map₁ ⟨$⟩ b)))
+           let open Setoid (T C (map₀ ∙ map₁ ⟨$⟩ a)) renaming (trans to _⟨≈⟩_) in
+           cong (trans₀ (map₁ ⟨$⟩ a)) (coh₁ p x≈y) ⟨≈⟩
+           coh₀ (cong map₁ p) (Setoid.refl (T B (map₁ ⟨$⟩ b)))
 
   ≈≈-refl : ∀ {A B} → Reflexive (_≈≈_ {A} {B})
   ≈≈-refl {B = B} = feq refl (reindex-refl B)
@@ -77,30 +82,30 @@ module _ {a b c d : Level} where
   ≈≈-sym : ∀ {A B} → Symmetric (_≈≈_ {A} {B})
   ≈≈-sym {A} {B} {F} {G} (feq g≈f φ≈γ) = feq (sym g≈f)
     λ {x} {bx} → Setoid.trans ( T B (map G ⟨$⟩ x) )
-      (Π.cong (reindex B (sym g≈f)) (Setoid.sym (T B (map F ⟨$⟩ x)) φ≈γ))
-      (left-inverse-of (reindex-sym B g≈f) (transport G x ⟨$⟩ bx))
+      (cong (reindex B (sym g≈f)) (Setoid.sym (T B (map F ⟨$⟩ x)) φ≈γ))
+      (strictlyInverseˡ (reindex-sym B g≈f) (transport G x ⟨$⟩ bx) )
     where
     open Setoid (U B) using (sym; Carrier)
     open Hom
-    open _InverseOf_
+    open IsInverse
 
   ≈≈-trans : ∀ {A B} → Transitive (_≈≈_ {A} {B})
   ≈≈-trans {A} {B} {F} {G} {H}  (feq ≈₁ t₁) (feq ≈₂ t₂) =
     feq (trans ≈₁ ≈₂) (λ {x} {bx} →
       let open Setoid (T B (Hom.map F ⟨$⟩ x)) renaming (trans to _⟨≈⟩_) in
-      reindex-trans B ≈₁ ≈₂ ⟨≈⟩ (Π.cong (reindex B ≈₁) t₂ ⟨≈⟩ t₁))
+      reindex-trans B ≈₁ ≈₂ ⟨≈⟩ (cong (reindex B ≈₁) t₂ ⟨≈⟩ t₁))
     where
     open Setoid (U B) using (trans)
 
   comp-resp-≈≈ : {A B C : Fam} {f h : Hom B C} {g i : Hom A B} →
       f ≈≈ h → g ≈≈ i → comp f g ≈≈ comp h i
   comp-resp-≈≈ {A} {B} {C} {f} {h} {g} {i} (feq f≈h t-f≈h) (feq g≈i t-g≈i) =
-    feq (trans (Π.cong (map f) g≈i) f≈h)
+    feq (trans (cong (map f) g≈i) f≈h)
         λ {x} → let open Setoid (T C (map (comp f g) ⟨$⟩ x)) renaming (trans to _⟨≈⟩_; sym to ≈sym) in
         reindex-trans C (cong (map f) g≈i) f≈h ⟨≈⟩
-        (Π.cong (reindex C (cong (map f) g≈i)) t-f≈h ⟨≈⟩
+        (cong (reindex C (cong (map f) g≈i)) t-f≈h ⟨≈⟩
         (≈sym (transport-coh {B} {C} f g≈i (Setoid.refl (T B (map i ⟨$⟩ x)))) ⟨≈⟩
-        Π.cong (transport f (map g ⟨$⟩ x)) t-g≈i))
+        cong (transport f (map g ⟨$⟩ x)) t-g≈i))
     where
     open _≈≈_
     open Setoid (U C)
@@ -126,7 +131,6 @@ module _ {a b c d : Level} where
     ; ∘-resp-≈ = comp-resp-≈≈
     }
     where
-    open _InverseOf_
     assoc′ : {A B C D : Fam} {f : Hom A B} {g : Hom B C} {h : Hom C D} →
       comp (comp h g) f ≈≈ comp h (comp g f)
     assoc′ {D = D} = feq (Setoid.refl (U D)) (reindex-refl D)
diff --git a/src/Categories/Category/Instance/Nat.agda b/src/Categories/Category/Instance/Nat.agda
index d4e5a9d1e..6afda4861 100644
--- a/src/Categories/Category/Instance/Nat.agda
+++ b/src/Categories/Category/Instance/Nat.agda
@@ -5,15 +5,16 @@ module Categories.Category.Instance.Nat where
 
 open import Level
 
-open import Data.Fin.Base using (Fin; inject+; raise; splitAt; join; remQuot; combine)
-open import Data.Fin.Properties
+open import Data.Fin.Base using (Fin; _↑ˡ_; _↑ʳ_; splitAt; join; remQuot; combine)
+open import Data.Fin.Properties using (join-splitAt; splitAt-↑ˡ; splitAt-↑ʳ; combine-remQuot;
+  remQuot-combine)
 open import Data.Nat.Base using (ℕ; _+_; _*_)
 open import Data.Product using (proj₁; proj₂; uncurry; <_,_>)
 open import Data.Sum using (inj₁; inj₂; [_,_]′)
-open import Data.Sum.Properties
+open import Data.Sum.Properties using ([,]-∘; [,]-cong)
 open import Relation.Binary.PropositionalEquality
   using (_≗_; _≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
-open import Function using (id; _∘′_; case_return_of_)
+open import Function using (id; _∘′_; case_returning_of_)
 
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
@@ -21,9 +22,9 @@ open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Duality using (Cocartesian⇒coCartesian; coCartesian⇒Cocartesian)
-open import Categories.Object.Coproduct
+open import Categories.Object.Coproduct using (Coproduct)
 open import Categories.Object.Duality using (Coproduct⇒coProduct; coProduct⇒Coproduct)
-open import Categories.Object.Product
+open import Categories.Object.Product using (Product)
 
 Nat : Category 0ℓ 0ℓ 0ℓ
 Nat = record
@@ -50,22 +51,22 @@ Nat = record
 Coprod : (m n : ℕ) → Coproduct Nat m n
 Coprod m n = record
   { A+B = m + n
-  ; i₁ = inject+ n
-  ; i₂ = raise m
+  ; i₁ = _↑ˡ n
+  ; i₂ = m ↑ʳ_
   ; [_,_] = λ l r z → [ l , r ]′ (splitAt m z)
-  ; inject₁ = λ {_ f g} x → cong [ f , g ]′ (splitAt-inject+ m n x)
-  ; inject₂ = λ {_ f g} x → cong [ f , g ]′ (splitAt-raise m n x)
+  ; inject₁ = λ {_ f g} x → cong [ f , g ]′ (splitAt-↑ˡ m x n)
+  ; inject₂ = λ {_ f g} x → cong [ f , g ]′ (splitAt-↑ʳ m n x)
   ; unique = uniq
   }
   where
     open ≡-Reasoning
     uniq : {o : ℕ} {h : Fin (m + n) → Fin o} {f : Fin m → Fin o} {g : Fin n → Fin o} →
-      h ∘′ inject+ n ≗ f → h ∘′ raise m ≗ g → (λ z → [ f , g ]′ (splitAt m z)) ≗ h
+      h ∘′ (_↑ˡ n) ≗ f → h ∘′ (m ↑ʳ_) ≗ g → (λ z → [ f , g ]′ (splitAt m z)) ≗ h
     uniq {_} {h} {f} {g} h≗f h≗g w = begin
-      [ f , g ]′ (splitAt m w)                         ≡˘⟨ [,]-cong h≗f h≗g (splitAt m w) ⟩
-      [ h ∘′ inject+ n , h ∘′ raise m ]′ (splitAt m w) ≡˘⟨ [,]-∘-distr h (splitAt m w) ⟩
-      h ([ inject+ n , raise m ]′ (splitAt m w))       ≡⟨ cong h (join-splitAt m n w) ⟩
-      h w                                              ∎
+      [ f , g ]′ (splitAt m w)                       ≡˘⟨ [,]-cong h≗f h≗g (splitAt m w) ⟩
+      [ h ∘′ (_↑ˡ n) , h ∘′ (m ↑ʳ_) ]′ (splitAt m w) ≡˘⟨ [,]-∘ h (splitAt m w) ⟩
+      h ([ _↑ˡ n , m ↑ʳ_ ]′ (splitAt m w))           ≡⟨ cong h (join-splitAt m n w) ⟩
+      h w                                            ∎
 
 Nat-Cocartesian : Cocartesian Nat
 Nat-Cocartesian = record
@@ -103,7 +104,7 @@ Nat-Cartesian = record
   { terminal = record
     { ⊤ = 1
     ; ⊤-is-terminal = record
-      { !-unique = λ f x → case f x return (Fin.zero ≡_) of λ { Fin.zero → refl }
+      { !-unique = λ f x → case f x returning (Fin.zero ≡_) of λ { Fin.zero → refl }
       }
     }
   ; products = record {product = λ {m} {n} → Prod m n }
diff --git a/src/Categories/Category/Instance/Properties/Setoids/CCC.agda b/src/Categories/Category/Instance/Properties/Setoids/CCC.agda
index b899ec62a..e59fddd75 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/CCC.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/CCC.agda
@@ -4,7 +4,8 @@ module Categories.Category.Instance.Properties.Setoids.CCC where
 
 open import Level
 open import Data.Product using (Σ ; _,_)
-open import Function.Equality as ⟶ using (Π; _⟶_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Setoid using (function)
 open import Relation.Binary using (Setoid)
 
 open import Categories.Category.Core using (Category)
@@ -15,8 +16,6 @@ open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesi
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Object.Terminal using (Terminal)
 
-open Π
-
 module _ ℓ where
   private
     S = Setoids ℓ ℓ
@@ -34,19 +33,19 @@ module _ ℓ where
     ; π₁-comp      = λ {_ _ f _ g} → project₁ {h = f} {g}
     ; π₂-comp      = λ {_ _ f _ g} → project₂ {h = f} {g}
     ; ⟨,⟩-unique   = λ {_ _ _ f g h} → unique {h = h} {f} {g}
-    ; _^_          = λ X Y → Y ⟶.⇨ X
+    ; _^_          = λ X Y → function Y X
     ; eval         = λ {X Y} → record
-      { _⟨$⟩_ = λ { (f , x) → f ⟨$⟩ x }
+      { to = λ { (f , x) → f ⟨$⟩ x }
       ; cong  = λ { (eq₁ , eq₂) → eq₁ eq₂ }
       }
     ; curry        = λ {C A B} f → record
-      { _⟨$⟩_ = λ c → record
-        { _⟨$⟩_ = λ a → f ⟨$⟩ (c , a)
-        ; cong  = λ eq → cong f (Setoid.refl C , eq)
+      { to = λ c → record
+        { to = λ a → f ⟨$⟩ (c , a)
+        ; cong  = λ eq → Func.cong f (Setoid.refl C , eq)
         }
-      ; cong  = λ eq₁ eq₂ → cong f (eq₁ , eq₂)
+      ; cong  = λ eq₁ eq₂ → Func.cong f (eq₁ , eq₂)
       }
-    ; eval-comp    = λ {_ _ _ f} → cong f
+    ; eval-comp    = λ {_ _ _ f} → Func.cong f
     ; curry-unique = λ eq₁ eq₂ eq → eq₁ (eq₂ , eq)
     }
     where
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Choice.agda b/src/Categories/Category/Instance/Properties/Setoids/Choice.agda
index 483c67e2a..f28432145 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/Choice.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/Choice.agda
@@ -5,20 +5,20 @@ module Categories.Category.Instance.Properties.Setoids.Choice where
 open import Categories.Category using (Category)
 open import Categories.Category.Exact using (Exact)
 open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Instance.Properties.Setoids.Exact using (SSurj)
+open import Categories.Object.InternalRelation using (Relation) 
 
+open import Data.Nat.Base using (ℕ)
 open import Data.Product using (∃; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_; map; zip; swap; map₂)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Function.Equality as SΠ using (Π; _⇨_) renaming (id to ⟶-id; _∘_ to _∘⟶_)
-
-open import Level
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Setoid using () renaming (function to _⇨_)
+open import Level using (Level; Lift)
 open import Relation.Binary using (Setoid; Rel; REL; IsEquivalence)
-import Relation.Binary.Reasoning.Setoid as SR
-
-open import Data.Nat.Base
 import Relation.Binary.PropositionalEquality.Core as P
+import Relation.Binary.Reasoning.Setoid as SR
 
 open Setoid renaming (_≈_ to [_][_≈_]; Carrier to ∣_∣) using (isEquivalence; refl; sym; trans)
-open Π using (_⟨$⟩_; cong)
 
 module _ ℓ where
   private
@@ -26,9 +26,6 @@ module _ ℓ where
     open Category S hiding (_≈_)
     module S = Category S
 
-  open import Categories.Category.Instance.Properties.Setoids.Exact
-  open import Categories.Object.InternalRelation using (Relation) 
-
   -- Presentation axiom, aka CoSHEP (https://ncatlab.org/nlab/show/presentation+axiom)
   record CoSHEP (A : Setoid ℓ ℓ) : Set (Level.suc ℓ) where
     field
@@ -45,12 +42,12 @@ module _ ℓ where
            ; isEquivalence = record { refl = P.refl ; sym = P.sym ; trans = P.trans }
            }
     ; pre = record
-           { _⟨$⟩_ = λ x → x
+           { to = λ x → x
            ; cong = λ {x} eq → P.subst (λ z → [ A ][ x ≈ z ]) eq (refl A)
            }
     ; surj = λ x → x , refl A
     ; split = λ {X} f surj → record
-           { _⟨$⟩_ = λ y → let x , _ = surj y in x
+           { to = λ y → let x , _ = surj y in x
            ; cong = λ {x}{y} x≡y → P.subst (λ z → [ X ][ proj₁ (surj x) ≈ proj₁ (surj z) ]) x≡y (refl X)
            }
            , λ {x}{y} x≡y → let z , eq = surj x in P.trans eq x≡y
@@ -65,7 +62,9 @@ module _ ℓ where
     where open Relation R
 
   ℕ-Setoid : Setoid ℓ ℓ
-  ℕ-Setoid = record { Carrier = Lift _ ℕ ; _≈_ = P._≡_  ; isEquivalence = record { refl = P.refl ; sym = P.sym ; trans = P.trans } }
+  ℕ-Setoid = record { Carrier = Lift _ ℕ ; _≈_ = P._≡_
+                    ; isEquivalence = record { refl = P.refl ; sym = P.sym ; trans = P.trans }
+                    }
 
   record DepChoice {A : Setoid ℓ ℓ} (R : Relation S A A) (inhb : ∣ A ∣) (ent : entire R) : Set (Level.suc ℓ) where
     open Relation R
@@ -94,7 +93,7 @@ module _ ℓ where
   -- Countable choice for setoids 
   ℕ-Choice :  ∀ {A : Setoid ℓ ℓ} (f : A ⇒ ℕ-Setoid) → SSurj ℓ f → Σ[ g ∈ ∣ ℕ-Setoid ⇨ A ∣ ] [ ℕ-Setoid ⇨ ℕ-Setoid ][ f ∘ g ≈ id ]
   ℕ-Choice {A} f surj = record
-    { _⟨$⟩_ = λ n → let x , eq = surj n in x
+    { to = λ n → let x , eq = surj n in x
     ; cong = λ {n}{m} eq → let x , _ = surj n; y , _ = surj m in P.subst (λ m → [ A ][ proj₁ (surj n) ≈ proj₁ (surj m) ]) eq (refl A) 
     }
     , λ {n}{m} n≡m → let _ , eq = surj n in P.trans eq n≡m
@@ -109,10 +108,10 @@ module _ ℓ where
       isfun  : ∀ (e : ∣ dom ∣) →  [ B ][ fun ⟨$⟩ (p₁ ⟨$⟩ e) ≈  p₂ ⟨$⟩ e ]
 
   Setoid-UniqueChoice :  {A B : Setoid ℓ ℓ} (R : Relation S A B) (ent : entire R) (frel : functional R) → UniqueChoice R ent frel
-  _⟨$⟩_ (UniqueChoice.fun (Setoid-UniqueChoice R ent frel)) x =  p₂ ⟨$⟩ proj₁ (ent x)
+  Func.to (UniqueChoice.fun (Setoid-UniqueChoice R ent frel)) x =  p₂ ⟨$⟩ proj₁ (ent x)
         where open Relation R
 
-  cong (UniqueChoice.fun (Setoid-UniqueChoice {A} {B} R ent frel)) {n} {m} n≈m =
+  Func.cong (UniqueChoice.fun (Setoid-UniqueChoice {A} {B} R ent frel)) {n} {m} n≈m =
      let (en , p₁en≈n) = ent n
          (em , p₁em≈m) = ent m in frel en em
      (begin
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda b/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda
index b5450582a..88589d7a4 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/Cocomplete.agda
@@ -2,26 +2,24 @@
 
 module Categories.Category.Instance.Properties.Setoids.Cocomplete where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Product using (Σ; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_)
-open import Function.Equality using (Π)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Relation.Binary using (Setoid; Preorder; Rel)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 open import Relation.Binary.Indexed.Heterogeneous using (_=[_]⇒_)
 open import Relation.Binary.Construct.Closure.SymmetricTransitive as ST using (Plus⇔; minimal)
 open Plus⇔
+open Func
 
 open import Categories.Category using (Category; _[_,_])
-open import Categories.Functor
-open import Categories.Category.Instance.Setoids
-open import Categories.Category.Cocomplete
+open import Categories.Functor.Core using (Functor)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Cocomplete using (Cocomplete)
 
 import Categories.Category.Construction.Cocones as Coc
 import Relation.Binary.Reasoning.Setoid as RS
 
-
-open Π using (_⟨$⟩_)
-
 module _ {o ℓ e} c ℓ′ {J : Category o ℓ e} (F : Functor J (Setoids (o ⊔ c) (o ⊔ ℓ ⊔ c ⊔ ℓ′))) where
   private
     module J    = Category J
@@ -39,7 +37,7 @@ module _ {o ℓ e} c ℓ′ {J : Category o ℓ e} (F : Functor J (Setoids (o 
   coc-preorder = record
     { Carrier    = vertex-carrier
     ; _≈_        = _≡_
-    ; _∼_        = coc
+    ; _≲_        = coc
     ; isPreorder = record
       { isEquivalence = ≡.isEquivalence
       ; reflexive     = λ { {j , _} ≡.refl → J.id , (identity (F₀.refl j)) }
@@ -47,7 +45,7 @@ module _ {o ℓ e} c ℓ′ {J : Category o ℓ e} (F : Functor J (Setoids (o 
         let open RS (F₀ c)
         in g J.∘ f , (begin
         F₁ (g J.∘ f) ⟨$⟩ Sa    ≈⟨ homomorphism (F₀.refl a) ⟩
-        F₁ g ⟨$⟩ (F₁ f ⟨$⟩ Sa) ≈⟨ Π.cong (F₁ g) eq₁ ⟩
+        F₁ g ⟨$⟩ (F₁ f ⟨$⟩ Sa) ≈⟨ cong (F₁ g) eq₁ ⟩
         F₁ g ⟨$⟩ Sb            ≈⟨ eq₂ ⟩
         Sc                     ∎) }
       }
@@ -61,10 +59,10 @@ Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record
       { N      = ⇛-Setoid
       ; coapex = record
         { ψ       = λ j → record
-          { _⟨$⟩_ = j ,_
+          { to = j ,_
           ; cong  = λ i≈k → forth (-, identity i≈k)
           }
-        ; commute = λ {X} X⇒Y x≈y → back (-, Π.cong (F₁ X⇒Y) (F₀.sym X x≈y))
+        ; commute = λ {X} X⇒Y x≈y → back (-, cong (F₁ X⇒Y) (F₀.sym X x≈y))
         }
       }
     ; ⊥-is-initial = record
@@ -72,10 +70,10 @@ Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record
         let module K = Cocone K
         in record
         { arr     = record
-          { _⟨$⟩_ = to-coapex K
+          { to = to-coapex K
           ; cong  = minimal (coc c ℓ′ F) K.N (to-coapex K) (coapex-cong K)
           }
-        ; commute = λ {X} x≈y → Π.cong (Coapex.ψ (Cocone.coapex K) X) x≈y
+        ; commute = λ {X} x≈y → cong (Coapex.ψ (Cocone.coapex K) X) x≈y
         }
       ; !-unique = λ { {K} f {a , Sa} {b , Sb} eq →
         let module K = Cocone K
@@ -83,7 +81,7 @@ Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record
             open RS K.N
         in begin
           K.ψ a ⟨$⟩ Sa       ≈˘⟨ f.commute (F₀.refl a) ⟩
-          f.arr ⟨$⟩ (a , Sa) ≈⟨ Π.cong f.arr eq ⟩
+          f.arr ⟨$⟩ (a , Sa) ≈⟨ cong f.arr eq ⟩
           f.arr ⟨$⟩ (b , Sb) ∎ }
       }
     }
@@ -104,7 +102,7 @@ Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record
         coapex-cong : ∀ K → coc c ℓ′ F =[ to-coapex K ]⇒ (Setoid._≈_ (Cocone.N K))
         coapex-cong K {X , x} {Y , y} (f , fx≈y) = begin
           K.ψ X ⟨$⟩ x            ≈˘⟨ K.commute f (F₀.refl X) ⟩
-          K.ψ Y ⟨$⟩ (F₁ f ⟨$⟩ x) ≈⟨ Π.cong (K.ψ Y) fx≈y ⟩
+          K.ψ Y ⟨$⟩ (F₁ f ⟨$⟩ x)  ≈⟨ cong (K.ψ Y) fx≈y ⟩
           K.ψ Y ⟨$⟩ y            ∎
           where module K = Cocone K
                 open RS K.N
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Complete.agda b/src/Categories/Category/Instance/Properties/Setoids/Complete.agda
index fd386cbd4..f48ced3a9 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/Complete.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/Complete.agda
@@ -2,10 +2,12 @@
 
 module Categories.Category.Instance.Properties.Setoids.Complete where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Product using (Σ; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_)
-open import Function.Equality using (Π)
-open import Relation.Binary using (Setoid; Rel)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Core using (Rel)
+open Func
 
 open import Categories.Category using (Category; _[_,_])
 open import Categories.Functor
@@ -14,8 +16,6 @@ open import Categories.Category.Complete
 
 import Categories.Category.Construction.Cones as Co
 
-open Π using (_⟨$⟩_)
-
 Setoids-Complete : (o ℓ e c ℓ′ : Level) → Complete o ℓ e (Setoids (c ⊔ ℓ ⊔ o ⊔ ℓ′) (o ⊔ ℓ′))
 Setoids-Complete o ℓ e c ℓ′ {J} F =
   record
@@ -33,7 +33,7 @@ Setoids-Complete o ℓ e c ℓ′ {J} F =
         }
       ;  apex = record
         { ψ = λ j → record
-          { _⟨$⟩_ = λ { (S , _) → S j }
+          { to = λ { (S , _) → S j }
           ; cong  = λ eq → eq j
           }
         ; commute = λ { {X} {Y} X⇒Y {_ , eq} {y} f≈g → F₀.trans Y (eq X⇒Y) (f≈g Y) }
@@ -44,10 +44,10 @@ Setoids-Complete o ℓ e c ℓ′ {J} F =
         let module K = Cone K
         in record
         { arr     = record
-          { _⟨$⟩_ = λ x → (λ j → K.ψ j ⟨$⟩ x) , λ f → K.commute f (Setoid.refl K.N)
-          ; cong  = λ a≈b j → Π.cong (K.ψ j) a≈b
+          { to = λ x → (λ j → K.ψ j ⟨$⟩ x) , λ f → K.commute f (Setoid.refl K.N)
+          ; cong  = λ a≈b j → cong (K.ψ j) a≈b
           }
-        ; commute = λ x≈y → Π.cong (K.ψ _) x≈y
+        ; commute = λ x≈y → cong (K.ψ _) x≈y
         }
       ; !-unique = λ {K} f x≈y j →
         let module K = Cone K
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda
index 0a8353e4a..ad0c42a10 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/Exact.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/Exact.agda
@@ -2,10 +2,27 @@
 
 module Categories.Category.Instance.Properties.Setoids.Exact where
 
+open import Data.Bool.Base using (Bool; true; false; T)
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.Fin using (Fin; zero) renaming (suc to nzero)
+open import Data.Product using (∃; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_; map; zip; swap; map₂)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Unit.Polymorphic.Base using (⊤; tt)
+open import Function using (flip) renaming (id to id→; _∘′_ to _∘→_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to ⟶-id)
+open import Function.Construct.Composition using (function)
+open import Function.Construct.Setoid using () renaming (function to _⇨_)
+open import Function.Definitions using (StrictlySurjective)
+open import Level using (Level)
+open import Relation.Binary using (Setoid; Rel; IsEquivalence)
+import Relation.Binary.Reasoning.Setoid as SR
+
 open import Categories.Category using (Category)
 open import Categories.Category.Exact using (Exact)
 open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical using (pullback; FiberProduct; mk-×; FP-≈)
 open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Regular using (Regular)
 open import Categories.Diagram.Coequalizer using (Coequalizer; IsCoequalizer; Coequalizer⇒Epi)
@@ -17,24 +34,8 @@ open import Categories.Morphism using (_≅_; Epi)
 open import Categories.Morphism.Regular using (RegularEpi)
 open import Categories.Object.InternalRelation using (Equivalence; EqSpan; KP⇒Relation; KP⇒EqSpan; KP⇒Equivalence; module Relation; rel)
 
-open import Data.Bool.Base using (Bool; true; false; T)
-open import Data.Empty.Polymorphic using (⊥)
-open import Data.Fin using (Fin; zero) renaming (suc to nzero)
-open import Data.Product using (∃; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_; map; zip; swap; map₂)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Data.Unit.Polymorphic.Base using (⊤; tt)
-open import Function using (flip) renaming (id to id→; _∘′_ to _∘→_)
-open import Function.Equality as SΠ using (Π; _⇨_) renaming (id to ⟶-id; _∘_ to _∘⟶_)
-open import Function.Definitions using (Surjective)
-open import Level
-open import Relation.Binary using (Setoid; Rel; IsEquivalence)
-import Relation.Binary.Reasoning.Setoid as SR
-
-open import Categories.Category.Instance.SingletonSet
-
 open Setoid renaming (_≈_ to [_][_≈_]; Carrier to ∣_∣) using (isEquivalence; refl; sym; trans)
-open Π using (_⟨$⟩_; cong)
-
+open Func
 
 module _ ℓ where
   private
@@ -42,6 +43,11 @@ module _ ℓ where
     open Category S hiding (_≈_)
     module S = Category S
 
+    infixr 9 _∙_
+    _∙_ : {a₁ a₂ b₁ b₂ c₁ c₂ : Level} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
+      {C : Setoid c₁ c₂} → Func B C → Func A B → Func A C
+    f ∙ g = function g f
+
   open Pullback using (P; p₁; p₂)
 
   -- the next bits all depend on a Setoid X and an Equivalence E, factor those out
@@ -77,8 +83,8 @@ module _ ℓ where
 
     quotient-trans {x₁} {x₂} {y₁} {y₂} (eqn eq x₁≈ ≈y₁) (eqn eq′ x₂≈ ≈y₂) x₁≈x₂ y₁≈y₂ =
       R.relation {SingletonSetoid}
-      (record { _⟨$⟩_ = λ _ → eq  ; cong = λ _ → refl R.dom})
-      (record { _⟨$⟩_ = λ _ → eq′ ; cong = λ _ → refl R.dom})
+      (record { to = λ _ → eq  ; cong = λ _ → refl R.dom})
+      (record { to = λ _ → eq′ ; cong = λ _ → refl R.dom})
       (λ { zero      _ → x₁≈ ○ x₁≈x₂ ○ ⟺ x₂≈
          ; (nzero _) _ → ≈y₁ ○ y₁≈y₂ ○ ⟺ ≈y₂}) tt
 
@@ -90,7 +96,7 @@ module _ ℓ where
         ; trans = λ { (eqn r x≈ ≈y) (eqn s y≈ ≈z) →
            let t = record { elem₁ = _ ; elem₂ = _ ; commute = y≈ ○ ⟺ ≈y } in
              eqn
-               (ES.trans ∘⟶ P₀⇒P₁ ⟨$⟩ t)
+               (ES.trans ∙ P₀⇒P₁ ⟨$⟩ t)
                (ES.is-trans₁ R×R.refl ○ (cong R.p₁ (p₂-≈ {t} {t} (D.refl , D.refl)) ○ x≈))
                (ES.is-trans₂ R×R.refl ○ (cong R.p₂ (p₁-≈ {t} {t} (D.refl , D.refl)) ○ ≈z))
            }
@@ -123,7 +129,7 @@ module _ ℓ where
 
         inj : X ⇒ X∼
         inj = record
-         { _⟨$⟩_ = id→
+         { to = id→
          ; cong = λ {x₁} eq → eqn (ES.refl ⟨$⟩ x₁) (ES.is-refl₁ X.refl) (ES.is-refl₂ X.refl ○ eq)
          }
 
@@ -133,7 +139,7 @@ module _ ℓ where
         -- coEqualizer wants the 'h' to be implicit, but can't figure it out, so make it explicit here
         quotient : {C : Obj} (h : X ⇒ C) → h ∘ R.p₁ S.≈ h ∘ R.p₂ → X∼ ⇒ C
         quotient {C} h eq = record
-          { _⟨$⟩_ = h ⟨$⟩_
+          { to = h ⟨$⟩_
           ; cong = λ { (eqn r x≈ ≈y) → trans C (cong h (X.sym x≈)) (trans C (eq (refl R.dom)) (cong h ≈y))}
           }
 
@@ -146,14 +152,13 @@ module _ ℓ where
           h ⟨$⟩ y ∎
           where open SR C
 
-  -- Setoid Surjectivity
+  -- Setoid (strict) Surjectivity
   SSurj : {A B : Setoid ℓ ℓ} (f : A ⇒ B) → Set ℓ
-  SSurj {A} {B} f = Surjective (Setoid._≈_ A) (Setoid._≈_ B) (f ⟨$⟩_)
+  SSurj {A} {B} f = StrictlySurjective (Setoid._≈_ B) (f ⟨$⟩_)
 
   -- Proposition 1 from "Olov Wilander, Setoids and universes"
   Epi⇒Surjective : ∀ {A B : Setoid ℓ ℓ} (f : A ⇒ B) → Epi S f → SSurj f
-  Epi⇒Surjective {A}{B} f epi y = g≈h (refl B {y}) .proj₁ (λ ()) _
-
+  Epi⇒Surjective {A} {B} f epi y = g≈h (refl B {y}) .proj₁ (λ ()) _
     where
       infix 3 _↔_
 
@@ -172,11 +177,11 @@ module _ ℓ where
         }
 
       g : B ⇒ B′
-      g = record { _⟨$⟩_ = λ x → false , x ; cong = λ _ → (λ _ ()) , (λ _ ()) }
+      g = record { to = λ x → false , x ; cong = λ _ → (λ _ ()) , (λ _ ()) }
 
       h : B ⇒ B′
       h = record
-          { _⟨$⟩_ = true ,_
+          { to = true ,_
           ; cong = λ x≈y →
                 (λ eq _ → map₂ (λ z → trans B z x≈y) (eq _))
               , (λ eq _ → let (a , eq′) = eq _ in a , (trans B eq′ (sym B x≈y)))
@@ -218,7 +223,7 @@ module _ ℓ where
               pt₁ : FiberProduct f f
               pt₁ = mk-× x₁ x₂ (trans B eq₁ (trans B y₁≈y₂ (sym B eq₂)))
           coeq : B S.⇒ C
-          coeq = record { _⟨$⟩_ = f⁻¹∘h ; cong = cong′ }
+          coeq = record { to = f⁻¹∘h ; cong = cong′ }
           universal′ : h S.≈ coeq S.∘ f
           universal′ {x} {y} x≈y = begin
             h ⟨$⟩ x                     ≈⟨ cong h x≈y ⟩
@@ -263,10 +268,10 @@ module _ ℓ where
       pb-of-re-is-re : {A B D : Setoid ℓ ℓ} (f : B ⇒ A) {u : D ⇒ A} →
         RegularEpi S f → (pb : Pullback S f u) → RegularEpi S (p₂ pb)
       pb-of-re-is-re {A}{B}{D} f {u} record { C = C ; h = _ ; g = _ ; coequalizer = coeq } pb =
-        Surjective⇒RegularEpi (p₂ pb) λ y →
+        Surjective⇒RegularEpi (p₂ pb) λ y → 
           let (x , eq) = Epi⇒Surjective f (Coequalizer⇒Epi S record { arr = f ; isCoequalizer = coeq }) (u ⟨$⟩ y) in
           let pt = mk-× x y eq in
-          P₀⇒P₁ ⟨$⟩ pt , p₂-≈ {pt} {pt} (refl B , refl D)
+          P₀⇒P₁ ⟨$⟩ pt , p₂-≈ {pt} {pt} (refl B , refl D) 
          where
 
            pb-fu : Pullback S f u
@@ -302,7 +307,7 @@ module _ ℓ where
           (eq : [ Z ⇨ Quotient-Setoid E ][ arr (Quotient-Coequalizer E) ∘ h₁ ≈ arr (Quotient-Coequalizer E) ∘ h₂ ]) →
           Z ⇒ Relation.dom (R E)
         universal {X}{Z} E h₁ h₂ eq = record
-          { _⟨$⟩_ = λ z → let (eqn eq _ _) = eq {z}{z} (refl Z) in eq
+          { to = λ z → let (eqn eq _ _) = eq {z}{z} (refl Z) in eq
           ; cong = λ {z}{z′} z≈z′ → quotient-trans E (eq {z}{z} (refl Z)) (eq {z′}{z′} (refl Z)) (cong h₁ z≈z′) (cong h₂ z≈z′)
           }
         p₁∘universal≈h₁ : {X Z : Setoid ℓ ℓ} → (E : Equivalence S X) → (h₁ h₂ : Z ⇒ X) →
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda
index 9879ce05c..2142fd2c9 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/Extensive.agda
@@ -2,12 +2,14 @@
 
 module Categories.Category.Instance.Properties.Setoids.Extensive where
 
-open import Level
-open import Data.Product using (∃; Σ; proj₁; proj₂; _,_; _×_)
+open import Level using (Level)
+open import Data.Product using (_,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂; _⊎ₛ_; drop-inj₁; drop-inj₂)
 open import Data.Unit.Polymorphic using (tt)
-open import Function.Equality using (Π; _⟶_; _⇨_; _∘_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Composition using (function)
+open import Function.Construct.Setoid using () renaming (function to _⇨_)
 open import Relation.Binary using (Setoid)
 import  Relation.Binary.Reasoning.Setoid as SetoidR
 
@@ -19,8 +21,8 @@ open import Categories.Diagram.Pullback using (Pullback)
 open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical using (pullback; FiberProduct)
 open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cocartesian)
 
-open Π
 open Pullback
+open Func
 
 -- Note the Setoids is extensive if the two levels coincide.  Whether it happens more generally
 -- is unknown at this point.
@@ -44,7 +46,7 @@ Setoids-Extensive ℓ = record
    ; disjoint = λ {A B} → record
         { commute = λ { {()} _}
         ; universal = λ {C f g} eq → record
-           { _⟨$⟩_ = λ z → conflict A B (eq {x = z} (refl (isEquivalence C)))
+           { to = λ z → conflict A B (eq {x = z} (refl (isEquivalence C)))
            ; cong = λ z → tt
            }
         ; unique = λ _ _ _ → tt
@@ -53,6 +55,11 @@ Setoids-Extensive ℓ = record
         }
    }
      where
+       infixr 9 _∙_
+       _∙_ : {a₁ a₂ b₁ b₂ c₁ c₂ : Level} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂}
+         {C : Setoid c₁ c₂} → Func B C → Func A B → Func A C
+       f ∙ g = function g f
+
        open Cocartesian (Setoids-Cocartesian {ℓ} {ℓ})
        open Relation.Binary.IsEquivalence
        open Setoid renaming (_≈_ to [_][_≈_]; Carrier to ∣_∣) using (isEquivalence)
@@ -62,8 +69,8 @@ Setoids-Extensive ℓ = record
          {x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≈ inj₂ y ] → Z
        conflict X Y ()
 
-       module Diagram {A B C X : Setoid ℓ ℓ} (f : C ⟶ A ⊎ₛ B)
-         (g : P (pullback ℓ ℓ f i₁) ⟶ X) (h : P (pullback ℓ ℓ f i₂) ⟶ X) where
+       module Diagram {A B C X : Setoid ℓ ℓ} (f : Func C (A ⊎ₛ B))
+         (g : Func (P (pullback ℓ ℓ f i₁)) X) (h : Func (P (pullback ℓ ℓ f i₂)) X) where
 
          private
            module A = Setoid A
@@ -80,9 +87,9 @@ Setoids-Extensive ℓ = record
            open SetoidR A⊎B′
 
          _⊎⟶_ : {o₁ o₂ o₃ ℓ₁ ℓ₂ ℓ₃ : Level} {X : Setoid o₁ ℓ₁} {Y : Setoid o₂ ℓ₂} {Z : Setoid o₃ ℓ₃} →
-           (X ⟶ Z) → (Y ⟶ Z) → (X ⊎ₛ Y) ⟶ Z
+           (Func X Z) → (Func Y Z) → Func (X ⊎ₛ Y) Z
          f₁ ⊎⟶ f₂ = record
-           { _⟨$⟩_ = Sum.[ f₁ ⟨$⟩_ , f₂ ⟨$⟩_ ]
+           { to = Sum.[ f₁ ⟨$⟩_ , f₂ ⟨$⟩_ ]
            ; cong = λ { (inj₁ x) → cong f₁ x ; (inj₂ x) → cong f₂ x}
            }
 
@@ -118,12 +125,12 @@ Setoids-Extensive ℓ = record
          f⟨$⟩-cong : {i j : ∣ C ∣} → i C.≈ j → [ A′ ⊎ₛ B′ ][ f⟨$⟩→ i ≈ f⟨$⟩→ j ]
          f⟨$⟩-cong {i} {j} i≈j = f⟨$⟩-cong′ i≈j (f ⟨$⟩ i) (f ⟨$⟩ j) A⊎B.refl A⊎B.refl
 
-         f⟨$⟩ : C ⟶ A′ ⊎ₛ B′
-         f⟨$⟩ = record { _⟨$⟩_ = f⟨$⟩→ ; cong = f⟨$⟩-cong }
+         f⟨$⟩ : Func C (A′ ⊎ₛ B′)
+         f⟨$⟩ = record { to = f⟨$⟩→ ; cong = f⟨$⟩-cong }
 
          -- copairing of g : A′ → X and h : B′ → X, resulting in C → X
-         copair : C ⟶ X
-         copair = (g ⊎⟶ h) ∘ f⟨$⟩
+         copair : Func C X
+         copair = (g ⊎⟶ h) ∙ f⟨$⟩
 
          copair-inject₁ : (z : FiberProduct f i₁) → [ X ][ copair ⟨$⟩ (FiberProduct.elem₁ z) ≈ g ⟨$⟩ z ]
          copair-inject₁ record { elem₁ = z ; elem₂ = x ; commute = eq } = cong (g ⊎⟶ h) (to-⊎ₛ-cong eq)
@@ -131,9 +138,9 @@ Setoids-Extensive ℓ = record
          copair-inject₂ : (z : FiberProduct f i₂) → [ X ][ copair ⟨$⟩ (FiberProduct.elem₁ z) ≈ h ⟨$⟩ z ]
          copair-inject₂ record { elem₁ = z ; elem₂ = y ; commute = eq } = cong (g ⊎⟶ h) (to-⊎ₛ-cong eq)
 
-         copair-unique′ : (u : C ⟶ X) (z : ∣ C ∣) →
-           [ A′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₁) ≈ g ] →
-           [ B′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₂) ≈ h ] →
+         copair-unique′ : (u : Func C X) (z : ∣ C ∣) →
+           [ A′ ⇨ X ][ u ∙ p₁ (pullback ℓ ℓ f i₁) ≈ g ] →
+           [ B′ ⇨ X ][ u ∙ p₁ (pullback ℓ ℓ f i₂) ≈ h ] →
            (w : ∣ A⊎B ∣) → [ A⊎B ][ f ⟨$⟩ z ≈ w ] →
            [ X ][ copair ⟨$⟩ z ≈ u ⟨$⟩ z ]
          copair-unique′ u z feq₁ feq₂ (inj₁ x) fz≈w = XR.begin
@@ -156,9 +163,9 @@ Setoids-Extensive ℓ = record
              module XR = SetoidR X
              fb = record {elem₁ = z ; elem₂ = y; commute = fz≈w }
 
-         copair-unique : (u : C ⟶ X) (z : ∣ C ∣) →
-           [ A′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₁) ≈ g ] →
-           [ B′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₂) ≈ h ] →
+         copair-unique : (u : Func C X) (z : ∣ C ∣) →
+           [ A′ ⇨ X ][ u ∙ p₁ (pullback ℓ ℓ f i₁) ≈ g ] →
+           [ B′ ⇨ X ][ u ∙ p₁ (pullback ℓ ℓ f i₂) ≈ h ] →
            [ X ][ copair ⟨$⟩ z ≈ u ⟨$⟩ z ]
          copair-unique u z feq₁ feq₂ = copair-unique′ u z (λ {x} {y} → feq₁ {x} {y}) (λ {x} {y} → feq₂ {x} {y}) (f ⟨$⟩ z) A⊎B.refl
 
diff --git a/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda b/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda
index 613a1b8f4..2801c56c8 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda
@@ -2,35 +2,34 @@
 
 module Categories.Category.Instance.Properties.Setoids.LCCC where
 
-open import Level
-open import Data.Product using (Σ; _,_)
-open import Function.Equality as Func using (Π; _⟶_)
+open import Level using (Level; _⊔_; 0ℓ; suc)
+open import Data.Product using (_,_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+import Function.Construct.Identity as FId
 open import Relation.Binary using (Setoid)
-import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡
 
-open import Categories.Category
-open import Categories.Category.BinaryProducts
-open import Categories.Category.CartesianClosed
+open import Categories.Category.Core using (Category)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.CartesianClosed using (CartesianClosed)
 open import Categories.Category.CartesianClosed.Canonical
   using (module Equivalence)
   renaming (CartesianClosed to Canonical)
 open import Categories.Category.CartesianClosed.Locally using (Locally)
-open import Categories.Category.Cartesian
+open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Instance.Span
-open import Categories.Category.Instance.Setoids
+  using (SpanObj; Span; span-id; left; right; span-arrʳ; span-arrˡ; center)
+open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Category.Instance.Properties.Setoids.Complete
-open import Categories.Category.Monoidal.Instance.Setoids
-open import Categories.Category.Slice
-open import Categories.Category.Slice.Properties
-open import Categories.Functor
-
-open import Categories.Object.Terminal
-open import Categories.Diagram.Pullback
-open import Categories.Diagram.Pullback.Limit
+  using (Setoids-Complete)
+open import Categories.Category.Slice using (Slice; sliceobj; slicearr; SliceObj; Slice⇒)
+open import Categories.Category.Slice.Properties using (pullback⇒product)
+open import Categories.Functor.Core using (Functor)
+open import Categories.Object.Terminal using (Terminal)
+open import Categories.Diagram.Pullback using (Pullback)
+open import Categories.Diagram.Pullback.Limit using (limit⇒pullback)
 import Categories.Object.Product as Prod
 
-open Π using (_⟨$⟩_)
-
 module _ {o ℓ} where
 
   module _ {A X : Setoid o ℓ} where
@@ -38,14 +37,14 @@ module _ {o ℓ} where
       module A = Setoid A
       module X = Setoid X
 
-    record InverseImage (a : Setoid.Carrier A) (f : X ⟶ A) : Set (o ⊔ ℓ) where
+    record InverseImage (a : Setoid.Carrier A) (f : Func X A) : Set (o ⊔ ℓ) where
       constructor pack
 
       field
         x    : X.Carrier
         fx≈a : f ⟨$⟩ x A.≈ a
 
-    inverseImage-transport : ∀ {a a′} {f : X ⟶ A} → a A.≈ a′ → InverseImage a f → InverseImage a′ f
+    inverseImage-transport : ∀ {a a′} {f : Func X A} → a A.≈ a′ → InverseImage a f → InverseImage a′ f
     inverseImage-transport eq img = pack x (A.trans fx≈a eq)
       where open InverseImage img
 
@@ -60,15 +59,15 @@ module _ {o ℓ} where
     --   f⁻¹(a) ⟶ g⁻¹(a)
     -- here, we need to take care of some coherence condition.
     record InverseImageMap (a : Setoid.Carrier A)
-                           (f : X ⟶ A)
-                           (g : Y ⟶ A) : Set (o ⊔ ℓ) where
+                           (f : Func X A)
+                           (g : Func Y A) : Set (o ⊔ ℓ) where
       field
         f⇒g  : InverseImage a f → InverseImage a g
         cong : ∀ (x x′ : InverseImage a f) →
                  InverseImage.x x X.≈ InverseImage.x x′ →
                  InverseImage.x (f⇒g x) Y.≈ InverseImage.x (f⇒g x′)
 
-    inverseImageMap-transport : ∀ {a a′} {f : X ⟶ A} {g : Y ⟶ A} → a A.≈ a′ →
+    inverseImageMap-transport : ∀ {a a′} {f : Func X A} {g : Func Y A} → a A.≈ a′ →
                                   InverseImageMap a f g → InverseImageMap a′ f g
     inverseImageMap-transport eq h = record
       { f⇒g  = λ img → inverseImage-transport eq (f⇒g (inverseImage-transport (A.sym eq) img))
@@ -76,8 +75,8 @@ module _ {o ℓ} where
       }
       where open InverseImageMap h
 
-    record SlExp (f : X ⟶ A)
-                 (g : Y ⟶ A) : Set (o ⊔ ℓ) where
+    record SlExp (f : Func X A)
+                 (g : Func Y A) : Set (o ⊔ ℓ) where
 
       field
         idx : A.Carrier
@@ -85,8 +84,8 @@ module _ {o ℓ} where
 
       open InverseImageMap map public
 
-    record SlExp≈ {f : X ⟶ A}
-                  {g : Y ⟶ A}
+    record SlExp≈ {f : Func X A}
+                  {g : Func Y A}
                   (h i : SlExp f g) : Set (o ⊔ ℓ) where
       private
         module h = SlExp h
@@ -98,7 +97,7 @@ module _ {o ℓ} where
         -- map≈′ : ∀ (img : InverseImage i.idx f) → InverseImage.x (i.f⇒g img) Y.≈ InverseImage.x (h.f⇒g (inverseImage-transport idx≈ img))
 
   SlExp-Setoid : ∀ {A X Y : Setoid o ℓ}
-                   (f : X ⟶ A) (g : Y ⟶ A) → Setoid (o ⊔ ℓ) (o ⊔ ℓ)
+                   (f : Func X A) (g : Func Y A) → Setoid (o ⊔ ℓ) (o ⊔ ℓ)
   SlExp-Setoid {A} {X} {Y} f g = record
     { Carrier       = SlExp f g
     ; _≈_           = SlExp≈
@@ -149,11 +148,11 @@ module _ {o} where
       slice-terminal : Terminal Sl
       slice-terminal = record
         { ⊤             = sliceobj {Y = A} record
-          { _⟨$⟩_ = λ x → x
+          { to = λ x → x
           ; cong  = λ eq → eq
           }
         ; ⊤-is-terminal = record
-          { !        = λ { {sliceobj f} → slicearr {h = f} (Π.cong f) }
+          { !        = λ { {sliceobj f} → slicearr {h = f} (Func.cong f) }
           ; !-unique = λ { {X} (slicearr △) eq →
                          let module X = SliceObj X
                          in sym (△ (Setoid.sym X.Y eq)) }
@@ -173,20 +172,20 @@ module _ {o} where
               F : Functor (Category.op Span) (Setoids o o)
               F = record
                 { F₀           = F₀ X Y
-                ; F₁           = λ { span-id   → Func.id
+                ; F₁           = λ { (span-id {B}) → FId.function (F₀ X Y B)
                                    ; span-arrˡ → X.arr
                                    ; span-arrʳ → Y.arr
                                    }
-                ; identity     = λ {Z} → S.Equiv.refl {F₀ X Y Z} {F₀ X Y Z} {Func.id}
+                ; identity     = λ {Z} → S.Equiv.refl {F₀ X Y Z} {F₀ X Y Z} {FId.function _}
                 ; homomorphism = λ { {_} {_} {_} {span-id}   {span-id}   eq → eq
-                                   ; {_} {_} {_} {span-id}   {span-arrˡ}    → Π.cong X.arr
-                                   ; {_} {_} {_} {span-id}   {span-arrʳ}    → Π.cong Y.arr
-                                   ; {_} {_} {_} {span-arrˡ} {span-id}      → Π.cong X.arr
-                                   ; {_} {_} {_} {span-arrʳ} {span-id}      → Π.cong Y.arr
+                                   ; {_} {_} {_} {span-id}   {span-arrˡ}    → Func.cong X.arr
+                                   ; {_} {_} {_} {span-id}   {span-arrʳ}    → Func.cong Y.arr
+                                   ; {_} {_} {_} {span-arrˡ} {span-id}      → Func.cong X.arr
+                                   ; {_} {_} {_} {span-arrʳ} {span-id}      → Func.cong Y.arr
                                    }
                 ; F-resp-≈     = λ { {_} {_} {span-id}   ≡.refl eq → eq
-                                   ; {_} {_} {span-arrˡ} ≡.refl    → Π.cong X.arr
-                                   ; {_} {_} {span-arrʳ} ≡.refl    → Π.cong Y.arr
+                                   ; {_} {_} {span-arrˡ} ≡.refl    → Func.cong X.arr
+                                   ; {_} {_} {span-arrʳ} ≡.refl    → Func.cong Y.arr
                                    }
                 }
 
@@ -209,7 +208,7 @@ module _ {o} where
 
       _^_ : Sl.Obj → Sl.Obj → Sl.Obj
       f ^ g = sliceobj {Y = SlExp-Setoid g.arr f.arr} record
-        { _⟨$⟩_ = SlExp.idx
+        { to = SlExp.idx
         ; cong  = SlExp≈.idx≈
         }
         where module f = SliceObj f
@@ -230,7 +229,7 @@ module _ {o} where
 
               h : SliceObj.Y (prod (f ^ g) g) S.⇒ f.Y
               h = record
-                { _⟨$⟩_ = λ { (J , arr) →
+                { to = λ { (J , arr) →
                   let module exp = SlExp (J left)
                   in InverseImage.x (exp.f⇒g (pack (J right) (trans (arr span-arrʳ) (sym (arr span-arrˡ))))) }
                 ; cong  = λ { {J₁ , arr₁} {J₂ , arr₂} eq →
@@ -278,7 +277,7 @@ module _ {o} where
                 ; cong = λ img img′ eq →
                   let module img  = InverseImage img
                       module img′ = InverseImage img′
-                  in Π.cong α.h λ { center → refl
+                  in Func.cong α.h λ { center → refl
                                   ; left   → fY.refl
                                   ; right  → eq }
                 }
@@ -286,22 +285,22 @@ module _ {o} where
 
             βcong : {i j : fY.Carrier} → i fY.≈ j → SlExp≈ (βmap i) (βmap j)
             βcong {i} {j} eq = record
-              { idx≈ = Π.cong f.arr eq
+              { idx≈ = Func.cong f.arr eq
               ; map≈ = λ img →
                 let open InverseImage img
-                in Π.cong α.h λ { center → Π.cong f.arr eq
+                in Func.cong α.h λ { center → Func.cong f.arr eq
                                 ; left   → eq
                                 ; right  → gY.refl }
               }
 
             β : f.Y S.⇒ SliceObj.Y (h ^ g)
             β = record
-              { _⟨$⟩_ = βmap
+              { to = βmap
               ; cong  = βcong
               }
 
           curry : f Sl.⇒ (h ^ g)
-          curry = slicearr {h = β} (Π.cong f.arr)
+          curry = slicearr {h = β} (Func.cong f.arr)
 
       module _ {f g h : Sl.Obj} {α β : prod f g Sl.⇒ h} where
         private
@@ -311,10 +310,10 @@ module _ {o} where
 
         curry-resp-≈ : α Sl.≈ β → curry α Sl.≈ curry β
         curry-resp-≈ eq eq′ = record
-          { idx≈ = Π.cong f.arr eq′
+          { idx≈ = Func.cong f.arr eq′
           ; map≈ = λ img →
             let open InverseImage img
-            in eq λ { center → Π.cong f.arr eq′
+            in eq λ { center → Func.cong f.arr eq′
                     ; left   → eq′
                     ; right  → gY.refl }
           }
@@ -336,9 +335,9 @@ module _ {o} where
           ; map≈ = λ img →
             let open InverseImage img
             in gY.trans (InverseImageMap.cong (SlExp.map (α.h ⟨$⟩ z)) img _ hY.refl)
-                        (eq {xypb z (inverseImage-transport (trans (α.△ eq′) (Π.cong f.arr (fY.sym eq′))) img)}
+                        (eq {xypb z (inverseImage-transport (trans (α.△ eq′) (Func.cong f.arr (fY.sym eq′))) img)}
                             {xypb w (inverseImage-transport (α.△ eq′) img)}
-                            λ { center → Π.cong f.arr eq′
+                            λ { center → Func.cong f.arr eq′
                               ; left   → eq′
                               ; right  → hY.refl })
           }
@@ -360,7 +359,7 @@ module _ {o} where
         ; curry        = curry
         ; eval-comp    = λ { {_} {_} {_} {α} {J , arr₁} eq →
           let module α = Slice⇒ α
-          in Π.cong α.h λ { center → trans (arr₁ span-arrˡ) (eq center)
+          in Func.cong α.h λ { center → trans (arr₁ span-arrˡ) (eq center)
                           ; left   → eq left
                           ; right  → eq right } }
         ; curry-unique = λ {_ _ _} {α β} → curry-unique {_} {_} {_} {α} {β}
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda
index f04c9ef23..650d73aad 100644
--- a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda
+++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda
@@ -8,21 +8,22 @@
 
 module Categories.Category.Instance.Properties.Setoids.Limits.Canonical where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Data.Product using (_,_; _×_; map; zip; proj₁; proj₂; <_,_>)
-open import Function.Equality as SΠ renaming (id to ⟶-id)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as SR
 
-open import Categories.Category.Instance.Setoids
-open import Categories.Diagram.Pullback
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Diagram.Pullback using (Pullback)
 
 open Setoid renaming (_≈_ to [_][_≈_])
+open Func
 
 --------------------------------------------------------------------------------
 -- Pullbacks
 
-record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) : Set (o ⊔ ℓ) where
+record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : Func X Z) (g : Func Y Z) : Set (o ⊔ ℓ) where
   constructor mk-×
   field
     elem₁ : Carrier X
@@ -31,10 +32,10 @@ record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) :
 
 open FiberProduct
 
-FP-≈ : ∀ {o ℓ} {X Y Z : Setoid o ℓ} {f : X ⟶ Z} {g : Y ⟶ Z} → (fb₁ fb₂ : FiberProduct f g) → Set ℓ
+FP-≈ : ∀ {o ℓ} {X Y Z : Setoid o ℓ} {f : Func X Z} {g : Func Y Z} → (fb₁ fb₂ : FiberProduct f g) → Set ℓ
 FP-≈ {X = X} {Y} p q = [ X ][ elem₁ p ≈ elem₁ q ] × [ Y ][ elem₂ p ≈ elem₂ q ]
 
-pullback : ∀ (o ℓ : Level) {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g
+pullback : ∀ (o ℓ : Level) {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : Func X Z) → (g : Func Y Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g
 pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
   { P = record
     { Carrier = FiberProduct f g
@@ -45,12 +46,12 @@ pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
       ; trans = zip X.trans Y.trans
       }
     }
-    ; p₁ = record { _⟨$⟩_ = elem₁ ; cong = proj₁ }
-    ; p₂ = record { _⟨$⟩_ = elem₂ ; cong = proj₂ }
+    ; p₁ = record { to = elem₁ ; cong = proj₁ }
+    ; p₂ = record { to = elem₂ ; cong = proj₂ }
     ; isPullback = record
       { commute = λ {p} {q} (eq₁ , eq₂) → trans Z (cong f eq₁) (commute q)
       ; universal = λ {A} {h₁} {h₂} eq → record
-        { _⟨$⟩_ = λ a → record
+        { to = λ a → record
           { elem₁ = h₁ ⟨$⟩ a
           ; elem₂ = h₂ ⟨$⟩ a
           ; commute = eq (refl A)
diff --git a/src/Categories/Category/Instance/Setoids.agda b/src/Categories/Category/Instance/Setoids.agda
index 332f430c1..04c6f8bea 100644
--- a/src/Categories/Category/Instance/Setoids.agda
+++ b/src/Categories/Category/Instance/Setoids.agda
@@ -4,24 +4,31 @@ module Categories.Category.Instance.Setoids where
 -- Category of Setoids, aka (Setoid, _⟶_, Setoid ≈)
 -- Note the (explicit) levels in each
 
-open import Level
-open import Relation.Binary
-open import Function.Equality as SΠ renaming (id to ⟶-id)
+open import Level using (suc; _⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Base using (_$_)
+import Function.Construct.Composition as Comp
+import Function.Construct.Identity as Id
+import Function.Construct.Setoid as S
 
-open import Categories.Category
+open import Categories.Category.Core using (Category)
+
+open Func
+open Setoid
 
 Setoids : ∀ c ℓ → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
 Setoids c ℓ = record
   { Obj       = Setoid c ℓ
-  ; _⇒_       = _⟶_
-  ; _≈_       = λ {A B} → Setoid._≈_ (A ⇨ B)
-  ; id        = ⟶-id
-  ; _∘_       = _∘_
-  ; assoc     = λ {_ _ _ D} {f g h} → cong (h ∘ g ∘ f)
-  ; sym-assoc = λ {_ _ _ D} {f g h} → cong (h ∘ g ∘ f)
-  ; identityˡ = λ {_ _} {f} → cong f
-  ; identityʳ = λ {_ _} {f} → cong f
-  ; identity² = λ eq → eq
-  ; equiv     = λ {A B} → Setoid.isEquivalence (A ⇨ B)
-  ; ∘-resp-≈  = λ f≡h g≡i x≡y → f≡h (g≡i x≡y)
+  ; _⇒_       = Func
+  ; _≈_       = λ {A} {B} f g → _≈_ (S.function A B) f g
+  ; id        = Id.function _
+  ; _∘_       = λ f g → Comp.function g f
+  ; assoc     = λ {A} {B} {C} {D} {f} {g} {h} x≈y → cong h $ cong g $ cong f x≈y
+  ; sym-assoc = λ {A} {B} {C} {D} {f} {g} {h} x≈y → cong h $ cong g $ cong f x≈y
+  ; identityˡ = λ {A} {B} {f} x≈y → cong f x≈y
+  ; identityʳ = λ {A} {B} {f} x≈y → cong f x≈y
+  ; identity² = λ x≈y → x≈y
+  ; equiv     = λ {A} {B} → isEquivalence (S.function A B)
+  ; ∘-resp-≈  = λ f≈f′ g≈g′ x≈y → f≈f′ (g≈g′ x≈y)
   }
diff --git a/src/Categories/Category/Instance/SimplicialSet/Properties.agda b/src/Categories/Category/Instance/SimplicialSet/Properties.agda
index 22c3b7517..1eb01e644 100644
--- a/src/Categories/Category/Instance/SimplicialSet/Properties.agda
+++ b/src/Categories/Category/Instance/SimplicialSet/Properties.agda
@@ -93,7 +93,7 @@ boundary-map {n = n} f b = record
       }
     }
   ; F₁ = λ f → record
-    { _⟨$⟩_ = λ (lift b) → lift (boundary-map f b)
+    { to = λ (lift b) → lift (boundary-map f b)
     ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
     }
   ; identity = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
@@ -135,7 +135,7 @@ record Horn (m n-1 : ℕ) (k : Fin (ℕ.suc n-1)) : Set where
       }
     }
   ; F₁ = λ f → record
-    { _⟨$⟩_ = λ (lift h) → lift record
+    { to = λ (lift h) → lift record
       { horn = boundary-map f (horn h)
       ; is-horn = is-horn h
       }
@@ -164,14 +164,14 @@ module _ where
   ∂Δ-inj : ∀ {n} → ∂Δ[ n ] ⇒ Δ[ n ]
   ∂Δ-inj {ℕ.zero} = ntHelper record
     { η = λ X → record
-      { _⟨$⟩_ = ⊥-elim
+      { to = ⊥-elim
       ; cong = λ { {()} }
       }
     ; commute = λ { _ {()} _ }
     }
   ∂Δ-inj {ℕ.suc n} = ntHelper record
     { η = λ X → record
-      { _⟨$⟩_ = λ (lift b) → lift (hom b)
+      { to = λ (lift b) → lift (hom b)
       ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
       }
     ; commute = λ f (lift eq) → lift (Δ-eq (Δ-pointwise eq))
@@ -183,7 +183,7 @@ module _ where
   Λ-inj : ∀ {n} → (k : Fin n) → Λ[ n , k ] ⇒ Δ[ n ]
   Λ-inj {n = ℕ.suc n} k = ntHelper record
     { η = λ X → record
-      { _⟨$⟩_ = λ (lift h) → lift (hom h)
+      { to = λ (lift h) → lift (hom h)
       ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
       }
     ; commute = λ f (lift eq) → lift (Δ-eq (Δ-pointwise eq))
diff --git a/src/Categories/Category/Monoidal/Closed/IsClosed.agda b/src/Categories/Category/Monoidal/Closed/IsClosed.agda
index 4029400fa..a0a5a38c0 100644
--- a/src/Categories/Category/Monoidal/Closed/IsClosed.agda
+++ b/src/Categories/Category/Monoidal/Closed/IsClosed.agda
@@ -1,47 +1,37 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Categories.Category
-open import Categories.Category.Monoidal
-open import Categories.Category.Monoidal.Closed
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Closed using (Closed)
 
 module Categories.Category.Monoidal.Closed.IsClosed
   {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (Cl : Closed M) where
 
-open import Data.Product using (Σ; _,_)
-open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality as Π using (Π)
+open import Data.Product using (_,_)
 
-open import Categories.Category.Product
-open import Categories.Category.Monoidal.Properties M
-open import Categories.Morphism C
-open import Categories.Morphism.Properties C
 open import Categories.Morphism.Reasoning C
-open import Categories.Functor renaming (id to idF)
-open import Categories.Functor.Bifunctor
-open import Categories.Functor.Bifunctor.Properties
-open import Categories.NaturalTransformation hiding (id)
-open import Categories.NaturalTransformation.Dinatural hiding (_∘ʳ_)
-open import Categories.NaturalTransformation.NaturalIsomorphism as NI hiding (refl)
+open import Categories.Functor using (Functor) renaming (id to idF)
+open import Categories.Functor.Bifunctor.Properties using ([_]-decompose₂)
 import Categories.Category.Closed as Cls
 
-open Closed Cl
+open Closed Cl using (adjoint; [_,_]₀; [_,_]₁; [-,-]; unit; unitorˡ; -⊗_;
+  module ⊗; [_,-]; [-,_])
 
 private
   module C = Category C
-  open Category C
-  open Commutation
+  open Category C using (module HomReasoning; Obj; _⇒_; id; _∘_; _≈_;
+    ∘-resp-≈ˡ; ∘-resp-≈ʳ)
   module ℱ = Functor
 
 open HomReasoning
-open Π.Π
-open adjoint renaming (unit to η; counit to ε)
+open adjoint using (Radjunct; Ladjunct; LRadjunct≈id; RLadjunct≈id; Radjunct-resp-≈) renaming (unit to η; counit to ε)
 
 -- and here we use sub-modules in the hopes of making things go faster
-open import Categories.Category.Monoidal.Closed.IsClosed.Identity Cl
-open import Categories.Category.Monoidal.Closed.IsClosed.L Cl
-open import Categories.Category.Monoidal.Closed.IsClosed.Dinatural Cl
-open import Categories.Category.Monoidal.Closed.IsClosed.Diagonal Cl
-open import Categories.Category.Monoidal.Closed.IsClosed.Pentagon Cl
+open import Categories.Category.Monoidal.Closed.IsClosed.Identity Cl using (identity; diagonal)
+open import Categories.Category.Monoidal.Closed.IsClosed.L Cl using (L; L-f-swap; L-g-swap)
+open import Categories.Category.Monoidal.Closed.IsClosed.Dinatural Cl using (L-dinatural-comm)
+open import Categories.Category.Monoidal.Closed.IsClosed.Diagonal Cl using (Lj≈j; jL≈i; iL≈i)
+open import Categories.Category.Monoidal.Closed.IsClosed.Pentagon Cl using (pentagon′)
 
 private
   id² : {S T : Obj} → [ S , T ]₀ ⇒ [ S , T ]₀
@@ -72,26 +62,21 @@ closed = record
   ; iL≈i             = iL≈i
   ; pentagon         = pentagon′
   ; γ⁻¹              = λ {X Y} → record
-    { _⟨$⟩_ = λ f → Radjunct f ∘ unitorˡ.to
+    { to = λ f → Radjunct f ∘ unitorˡ.to
     ; cong  = λ eq → ∘-resp-≈ˡ (∘-resp-≈ʳ (ℱ.F-resp-≈ (-⊗ X) eq))
     }
-  ; γ-inverseOf-γ⁻¹  = λ {X Y} → record
-    { left-inverse-of  = λ f → begin
-      [ id , Radjunct f ∘ unitorˡ.to ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit
-        ≈⟨ ℱ.homomorphism [ X ,-] ⟩∘⟨refl ⟩
-      ([ id , Radjunct f ]₁ ∘ [ id , unitorˡ.to ]₁) ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit
-        ≈⟨ cancelInner (⟺ (ℱ.homomorphism [ X ,-]) ○ ℱ.F-resp-≈ [ X ,-] unitorˡ.isoˡ ○ [-,-].identity) ⟩
-      Ladjunct (Radjunct f) ≈⟨ LRadjunct≈id ⟩
-      f
-        ∎
-    ; right-inverse-of = λ f → begin
-      Radjunct ([ id , f ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit) ∘ unitorˡ.to
-        ≈˘⟨ ∘-resp-≈ʳ (ℱ.F-resp-≈ (-⊗ X) (pushˡ (ℱ.homomorphism [ X ,-]))) ⟩∘⟨refl ⟩
-      Radjunct (Ladjunct (f ∘ unitorˡ.from)) ∘ unitorˡ.to
-        ≈⟨ RLadjunct≈id ⟩∘⟨refl ⟩
-      (f ∘ unitorˡ.from) ∘ unitorˡ.to
-        ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
-      f
-        ∎
-    }
+  ; γ-γ⁻¹-inverseᵇ  = λ {X Y} →
+    (λ {f} {y} eq →  begin
+      Radjunct y ∘ unitorˡ.to                                                    ≈⟨ Radjunct-resp-≈ eq ⟩∘⟨refl ⟩
+      Radjunct ( [ id , f ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit) ∘ unitorˡ.to   ≈˘⟨ Radjunct-resp-≈ (pushˡ (ℱ.homomorphism [ X ,-])) ⟩∘⟨refl ⟩
+      Radjunct (Ladjunct (f ∘ unitorˡ.from)) ∘ unitorˡ.to                        ≈⟨ RLadjunct≈id ⟩∘⟨refl ⟩
+      (f ∘ unitorˡ.from) ∘ unitorˡ.to                                            ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
+      f ∎
+      ) ,
+    λ {y} {f} eq → begin
+      [ id , f ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit                                   ≈⟨ [-,-].F-resp-≈ (C.Equiv.refl , eq) ⟩∘⟨refl ⟩
+      [ id , Radjunct y ∘ unitorˡ.to ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit             ≈⟨ ℱ.homomorphism [ X ,-] ⟩∘⟨refl ⟩
+      ([ id , Radjunct y ]₁ ∘ [ id , unitorˡ.to ]₁) ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit ≈⟨ cancelInner (⟺ (ℱ.homomorphism [ X ,-]) ○ ℱ.F-resp-≈ [ X ,-] unitorˡ.isoˡ ○ [-,-].identity) ⟩
+      Ladjunct (Radjunct y)                                                             ≈⟨ LRadjunct≈id ⟩
+      y ∎
   }
diff --git a/src/Categories/Category/Monoidal/Closed/IsClosed/Diagonal.agda b/src/Categories/Category/Monoidal/Closed/IsClosed/Diagonal.agda
index d994c3c4c..3774ab16d 100644
--- a/src/Categories/Category/Monoidal/Closed/IsClosed/Diagonal.agda
+++ b/src/Categories/Category/Monoidal/Closed/IsClosed/Diagonal.agda
@@ -9,7 +9,6 @@ module Categories.Category.Monoidal.Closed.IsClosed.Diagonal
 
 open import Data.Product using (Σ; _,_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality as Π using (Π)
 
 open import Categories.Category.Product
 open import Categories.Category.Monoidal.Properties M
@@ -38,7 +37,6 @@ private
 
 open HomReasoning
 open Equiv
-open Π.Π
 open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃; Ladjunct-comm′ to 𝕃-comm′;
  Ladjunct-resp-≈ to 𝕃-resp-≈)
 
diff --git a/src/Categories/Category/Monoidal/Closed/IsClosed/Dinatural.agda b/src/Categories/Category/Monoidal/Closed/IsClosed/Dinatural.agda
index 25b1eea98..68a1b7376 100644
--- a/src/Categories/Category/Monoidal/Closed/IsClosed/Dinatural.agda
+++ b/src/Categories/Category/Monoidal/Closed/IsClosed/Dinatural.agda
@@ -9,7 +9,6 @@ module Categories.Category.Monoidal.Closed.IsClosed.Dinatural
 
 open import Data.Product using (Σ; _,_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality as Π using (Π)
 
 open import Categories.Category.Product
 open import Categories.Category.Monoidal.Properties M
@@ -34,7 +33,6 @@ private
 
 open HomReasoning
 open Equiv
-open Π.Π
 open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃; Ladjunct-comm′ to 𝕃-comm′;
  Ladjunct-resp-≈ to 𝕃-resp-≈)
 
diff --git a/src/Categories/Category/Monoidal/Closed/IsClosed/L.agda b/src/Categories/Category/Monoidal/Closed/IsClosed/L.agda
index 3a1ba0417..c26fdcbde 100644
--- a/src/Categories/Category/Monoidal/Closed/IsClosed/L.agda
+++ b/src/Categories/Category/Monoidal/Closed/IsClosed/L.agda
@@ -9,7 +9,6 @@ module Categories.Category.Monoidal.Closed.IsClosed.L
 
 open import Data.Product using (_,_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality as Π using (Π)
 
 open import Categories.Morphism.Reasoning C
   using (pull-last; pull-first; pullˡ; pushˡ; center; center⁻¹; pullʳ)
@@ -26,7 +25,6 @@ private
   α⇒ = associator.from
   α⇐ = associator.to
 
-open Π.Π
 open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃; Ladjunct-comm′ to 𝕃-comm′;
  Ladjunct-resp-≈ to 𝕃-resp-≈)
 
diff --git a/src/Categories/Category/Monoidal/Closed/IsClosed/Pentagon.agda b/src/Categories/Category/Monoidal/Closed/IsClosed/Pentagon.agda
index 91de81a11..c6f74ed51 100644
--- a/src/Categories/Category/Monoidal/Closed/IsClosed/Pentagon.agda
+++ b/src/Categories/Category/Monoidal/Closed/IsClosed/Pentagon.agda
@@ -9,7 +9,6 @@ module Categories.Category.Monoidal.Closed.IsClosed.Pentagon
 
 open import Data.Product using (Σ; _,_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality as Π using (Π)
 
 open import Categories.Category.Product
 open import Categories.Category.Monoidal.Properties M
@@ -40,7 +39,6 @@ private
 
 open HomReasoning
 open Equiv
-open Π.Π
 open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃; Ladjunct-comm′ to 𝕃-comm′;
  Ladjunct-resp-≈ to 𝕃-resp-≈)
 
diff --git a/src/Categories/Category/Monoidal/Instance/Setoids.agda b/src/Categories/Category/Monoidal/Instance/Setoids.agda
index a7efda1a2..4edc6cdb4 100644
--- a/src/Categories/Category/Monoidal/Instance/Setoids.agda
+++ b/src/Categories/Category/Monoidal/Instance/Setoids.agda
@@ -2,22 +2,24 @@
 
 module Categories.Category.Monoidal.Instance.Setoids where
 
-open import Level
-open import Data.Product
-open import Data.Product.Relation.Binary.Pointwise.NonDependent
-open import Data.Sum
-open import Data.Sum.Relation.Binary.Pointwise
-open import Function.Equality
+open import Level using (_⊔_; suc)
+open import Data.Product.Base using (proj₁; proj₂; _,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
+open import Data.Sum.Base using ([_,_]; inj₁; inj₂)
+open import Data.Sum.Relation.Binary.Pointwise using (⊎-setoid; inj₁; inj₂)
+open import Function.Bundles using (_⟨$⟩_; Func)
 open import Relation.Binary using (Setoid)
 
-open import Categories.Category
-open import Categories.Category.Instance.Setoids
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
 open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
-open import Categories.Category.Cocartesian
-open import Categories.Category.Instance.SingletonSet
-open import Categories.Category.Instance.EmptySet
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Category.Instance.SingletonSet using (SingletonSetoid-⊤)
+open import Categories.Category.Instance.EmptySet using (EmptySetoid-⊥)
+
+open Func
 
 module _ {o ℓ} where
 
@@ -31,15 +33,15 @@ module _ {o ℓ} where
          in record
           { A×B      = ×-setoid A B -- the stdlib doesn't provide projections!
           ; π₁       = record
-            { _⟨$⟩_ = proj₁
+            { to = proj₁
             ; cong  = proj₁
             }
           ; π₂       = record
-            { _⟨$⟩_ = proj₂
+            { to = proj₂
             ; cong  = proj₂
             }
           ; ⟨_,_⟩    = λ f g → record
-            { _⟨$⟩_ = λ x → f ⟨$⟩ x , g ⟨$⟩ x
+            { to = λ x → f ⟨$⟩ x , g ⟨$⟩ x
             ; cong  = λ eq → cong f eq , cong g eq
             }
           ; project₁ = λ {_ h i} eq → cong h eq
@@ -60,14 +62,14 @@ module _ {o ℓ} where
     ; coproducts = record
       { coproduct = λ {A} {B} → record
         { A+B = ⊎-setoid A B
-        ; i₁ = record { _⟨$⟩_ = inj₁ ; cong = inj₁ }
-        ; i₂ = record { _⟨$⟩_ = inj₂ ; cong = inj₂ }
+        ; i₁ = record { to = inj₁ ; cong = inj₁ }
+        ; i₂ = record { to = inj₂ ; cong = inj₂ }
         ; [_,_] = λ f g → record
-          { _⟨$⟩_ = [ f ⟨$⟩_ , g ⟨$⟩_ ]
-          ; cong = λ { (inj₁ x) → Π.cong f x ; (inj₂ x) → Π.cong g x }
+          { to = [ f ⟨$⟩_ , g ⟨$⟩_ ]
+          ; cong = λ { (inj₁ x) → cong f x ; (inj₂ x) → cong g x }
           }
-        ; inject₁ = λ {_} {f} → Π.cong f
-        ; inject₂ = λ {_} {_} {g} → Π.cong g
+        ; inject₁ = λ {_} {f} → cong f
+        ; inject₂ = λ {_} {_} {g} → cong g
         ; unique = λ { {C} h≈f h≈g (inj₁ x) → Setoid.sym C (h≈f (Setoid.sym A x))
                      ; {C} h≈f h≈g (inj₂ x) → Setoid.sym C (h≈g (Setoid.sym B x)) }
         }
diff --git a/src/Categories/Category/Monoidal/Instance/Sets.agda b/src/Categories/Category/Monoidal/Instance/Sets.agda
index ca37fffcc..ea5ba2947 100644
--- a/src/Categories/Category/Monoidal/Instance/Sets.agda
+++ b/src/Categories/Category/Monoidal/Instance/Sets.agda
@@ -9,9 +9,7 @@ open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry; map; <
 open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Unit using (⊤)
 open import Relation.Binary.PropositionalEquality.Core
-open import Function.Inverse using (module Inverse; _↔_)
 open import Function.Related.TypeIsomorphisms
-open import Function.Equality using () renaming (_⟨$⟩_ to fun)
 open import Function using (_$_)
 
 open import Categories.Category.BinaryProducts using (BinaryProducts)
diff --git a/src/Categories/Category/Species/Constructions.agda b/src/Categories/Category/Species/Constructions.agda
index 281f6f41c..571f499f8 100644
--- a/src/Categories/Category/Species/Constructions.agda
+++ b/src/Categories/Category/Species/Constructions.agda
@@ -7,22 +7,17 @@ open import Level
 open import Data.Empty
 open import Data.Fin.Base as Fin using (Fin)
 open import Data.Fin.Properties using (¬Fin0)
-open import Data.Fin.Permutation using (↔⇒≡)
 open import Data.Nat.Base using (ℕ; suc; zero)
-open import Data.Nat.Properties using (_≟_)
 open import Data.Product as × using (Σ; proj₁; proj₂; _,_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
 open import Data.Sum.Base as ⊎ using (inj₁; inj₂)
 open import Data.Sum.Relation.Binary.Pointwise using (_⊎ₛ_; inj₁; inj₂)
 open import Data.Unit.Polymorphic using (⊤; tt)
 open import Function.Base using () renaming (id to id→)
-open import Function.Equality using (_⟨$⟩_; cong; Π) renaming (id to idΠ)
-open import Function.Bundles using (Inverse)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Relation.Nullary using (Dec; yes; no)
-import Function.Inverse as Inv
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.PropositionalEquality as ≡
-open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial using (indexedSetoid)
 
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Construction.ObjectRestriction using (ObjectRestriction)
@@ -56,11 +51,11 @@ module _ {o ℓ : Level} where
     ⊤-Setoid ,
     1 ,
     record
-      { f = λ _ → Fin.zero
-      ; f⁻¹ = λ _ → tt
-      ; cong₁ = λ _ → ≡.refl
-      ; cong₂ = λ _ → tt
-      ; inverse = (λ { Fin.zero → ≡.refl}) , λ _ → tt
+      { to = λ _ → Fin.zero
+      ; from = λ _ → tt
+      ; to-cong = λ _ → ≡.refl
+      ; from-cong = λ _ → tt
+      ; inverse = (λ { {Fin.zero} _ → ≡.refl }) , λ _ → tt
       }
 
 -- We could have 4 levels, and still define Zero and One′.
@@ -84,73 +79,8 @@ module _ (o : Level) where
   Zero = const ⊥-Setoid
 
   -- One can be specified in two ways.  The traditional one (which doesn't generalize as well)
-  -- uses 'counting' directly.
-  One′ : Structure
-  One′ = record
-    { F₀ = on-singleton
-    ; F₁ = map-singleton
-    ; identity = λ {A} x≈y → identity′ {A} x≈y -- eta expansion needed
-    ; homomorphism = λ {X} {Y} {Z} → homomorphism′ {X} {Y} {Z} -- eta needed
-    ; F-resp-≈ = resp
-    }
-    where
-
-    iso⇒Inverse : (A B : Σ S IsFiniteSetoid) (A≅B : A ≅ B) → Inverse (proj₁ A) (proj₁ B)
-    iso⇒Inverse (s , n , p) (s′ , n′ , p′) A≅B = record
-      { f = from A≅B ⟨$⟩_
-      ; f⁻¹ = to A≅B ⟨$⟩_
-      ; cong₁ = cong (from A≅B)
-      ; cong₂ = cong (to A≅B)
-      ; inverse = (λ x → isoʳ A≅B (Setoid.refl s′ {x})) , λ x → isoˡ A≅B (Setoid.refl s {x})
-      }
-
-    iso⇒≡ : {A B : Σ S IsFiniteSetoid} (A≅B : A ≅ B) → proj₁ (proj₂ A) ≡.≡ proj₁ (proj₂ B)
-    iso⇒≡ {A@(s , n , p)} {B@(s′ , n′ , p′)} A≅B = ↔⇒≡ ( (translate p′) Inv.∘ (translate X Inv.∘ Inv.sym (translate p)))
-      where
-      X : Inverse (proj₁ A) (proj₁ B)
-      X = iso⇒Inverse A B A≅B
-      translate : {a b c d : Level} {X : Setoid a b} {Y : Setoid c d} → Inverse X Y → Inv.Inverse X Y
-      translate I = record
-        { to = record { _⟨$⟩_ = Inverse.f I ; cong = Inverse.cong₁ I }
-        ; from = record { _⟨$⟩_ = Inverse.f⁻¹ I ; cong = Inverse.cong₂ I }
-        ; inverse-of = record
-          { left-inverse-of = Inverse.inverseʳ I
-          ; right-inverse-of = Inverse.inverseˡ I
-          }
-        }
-
-    -- one can do this in 3 cases structurally, but that leads to 9 cases elsewhere
-    -- so a dispatch on size makes sense
-    on-singleton : Σ S IsFiniteSetoid → S
-    on-singleton (s , n , _) with n ≟ 1
-    ... | yes p = s
-    ... | no ¬p = ⊥-Setoid
-
-    map-singleton : {A B : Σ S IsFiniteSetoid} → A ≅ B → Π (on-singleton A) (indexedSetoid (on-singleton B))
-    map-singleton {s , n , p} {s′ , n′ , p′} A≅B with n ≟ 1 | n′ ≟ 1
-    map-singleton A≅B | yes ≡.refl | yes ≡.refl = from A≅B
-    map-singleton A≅B | yes ≡.refl | no  n′≢1    = ⊥-elim (n′≢1 (≡.sym (iso⇒≡ A≅B)))
-    map-singleton A≅B | no  n≢1    | yes n′≡1    = ⊥-elim (n≢1 (≡.trans (iso⇒≡ A≅B) n′≡1))
-    map-singleton A≅B | no  n≢1    | no  n′≢1    = idΠ
-
-    identity′ : {A : Σ S IsFiniteSetoid} {x y : Setoid.Carrier (on-singleton A)} →
-      let SA = on-singleton A in
-      Setoid._≈_ SA x y → Setoid._≈_ SA (map-singleton {A} {A} ≅.refl ⟨$⟩ x) y
-    identity′ {s , ℕ.suc ℕ.zero , p} x≈y = x≈y
-
-    homomorphism′ : {X Y Z : Σ S IsFiniteSetoid} {f : X ≅ Y} {g : Y ≅ Z} {x y : Setoid.Carrier (on-singleton X)} →
-      Setoid._≈_ (on-singleton X) x y →
-      Setoid._≈_ (on-singleton Z) (map-singleton (≅.trans f g) ⟨$⟩ x) (map-singleton g ⟨$⟩ (map-singleton f ⟨$⟩ y))
-    homomorphism′ {f = f} {g} x≈y with iso⇒≡ f | iso⇒≡ g
-    homomorphism′ {_ , 1 , _} {f = f} {g} x≈y | ≡.refl | ≡.refl = cong (from g) (cong (from f) x≈y)
-
-    resp : {A B : Σ S IsFiniteSetoid} {f g : A ≅ B} →
-      (_≃_ FinSet f g) →
-      {x y : Setoid.Carrier (on-singleton A)} →
-      Setoid._≈_ (on-singleton A) x y → Setoid._≈_ (on-singleton B) (map-singleton f ⟨$⟩ x) (map-singleton g ⟨$⟩ y)
-    resp {_ , 1 , _} {f = f} {g} f≈g x≈y with iso⇒≡ f
-    resp {_ , 1 , _} {f = f} {g} f≈g x≈y | ≡.refl = _≃_.from-≈ f≈g x≈y
-
+  -- uses 'counting' directly. Don't even try it here, it just leads to much pain.
+  
   -- There is a much nicer specification.
   One : Structure
   One = Hom[ 𝔹 ][ ⊤-FinSetoid ,-]
@@ -160,10 +90,10 @@ module _ (o : Level) where
   X = record
     { F₀ = proj₁
     ; F₁ = λ f → record
-        { _⟨$⟩_ = from f ⟨$⟩_
-        ; cong = cong (from f) }
+        { to = from f ⟨$⟩_
+        ; cong = Func.cong (from f) }
     ; identity = id→
-    ; homomorphism = λ { {f = f} {g} x≈y → cong (from g) (cong (from f) x≈y)}
+    ; homomorphism = λ { {f = f} {g} x≈y → Func.cong (from g) (Func.cong (from f) x≈y)}
     ; F-resp-≈ = _≃_.from-≈
     }
 
@@ -172,9 +102,9 @@ module _ (o : Level) where
   A + B = record
     { F₀ = λ x → A.₀ x ⊎ₛ B.₀ x
     ; F₁ = λ X≅Y → record
-      { _⟨$⟩_ = ⊎.map (A.₁ X≅Y ⟨$⟩_) (B.₁ X≅Y ⟨$⟩_)
-      ; cong = λ { (inj₁ x≈y) → inj₁ (cong (A.₁ X≅Y) x≈y )
-                 ; (inj₂ x≈y) → inj₂ (cong (B.₁ X≅Y) x≈y)}
+      { to = ⊎.map (A.₁ X≅Y ⟨$⟩_) (B.₁ X≅Y ⟨$⟩_)
+      ; cong = λ { (inj₁ x≈y) → inj₁ (Func.cong (A.₁ X≅Y) x≈y )
+                 ; (inj₂ x≈y) → inj₂ (Func.cong (B.₁ X≅Y) x≈y)}
       }
     ; identity = λ { (inj₁ x) → inj₁ (A.identity x)
                    ; (inj₂ x) → inj₂ (B.identity x)}
@@ -192,8 +122,8 @@ module _ (o : Level) where
   A × B = record
     { F₀ = λ x → ×-setoid (A.₀ x) (B.₀ x)
     ; F₁ = λ X≅Y → record
-      { _⟨$⟩_ = ×.map (A.₁ X≅Y ⟨$⟩_) (B.₁ X≅Y ⟨$⟩_)
-      ; cong = ×.map (cong (A.₁ X≅Y)) (cong (B.₁ X≅Y))
+      { to = ×.map (A.₁ X≅Y ⟨$⟩_) (B.₁ X≅Y ⟨$⟩_)
+      ; cong = ×.map (Func.cong (A.₁ X≅Y)) (Func.cong (B.₁ X≅Y))
       }
     ; identity = ×.map A.identity B.identity
     ; homomorphism = ×.map A.homomorphism B.homomorphism
diff --git a/src/Categories/Category/Unbundled/Properties.agda b/src/Categories/Category/Unbundled/Properties.agda
index 563f8cf51..eccdc3bb5 100644
--- a/src/Categories/Category/Unbundled/Properties.agda
+++ b/src/Categories/Category/Unbundled/Properties.agda
@@ -6,7 +6,7 @@ module Categories.Category.Unbundled.Properties where
 
 open import Data.Product using (Σ; _,_)
 open import Level
-open import Function using (_↔_; mk↔′)
+open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Relation.Binary.PropositionalEquality using (refl)
 
 open import Categories.Category.Core using (Category)
@@ -33,4 +33,4 @@ pack′ {Obj = o} uc  = record { Obj = o; UC }
   where module UC = Unb-Cat uc
 
 equiv : (Category o ℓ e) ↔ (Σ (Set o) (λ Obj → Unb-Cat Obj ℓ e))
-equiv = mk↔′ unpack pack (λ _ → refl) λ _ → refl
+equiv = mk↔ₛ′ unpack pack (λ _ → refl) λ _ → refl
diff --git a/src/Categories/CoYoneda.agda b/src/Categories/CoYoneda.agda
index 8310bc4d7..7c602bec6 100644
--- a/src/Categories/CoYoneda.agda
+++ b/src/Categories/CoYoneda.agda
@@ -3,10 +3,9 @@ module Categories.CoYoneda where
 
 -- CoYoneda Lemma.  See Yoneda for more documentation
 
-open import Level
+open import Level using (Level; _⊔_; lift; lower)
 open import Function.Base using (_$_)
-open import Function.Bundles using (Inverse)
-open import Function.Equality using (Π; _⟨$⟩_; cong)
+open import Function.Bundles using (Inverse; Func; _⟨$⟩_)
 open import Relation.Binary.Bundles using (module Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidR
 open import Data.Product using (_,_; Σ)
@@ -15,7 +14,7 @@ open import Categories.Category using (Category; _[_,_])
 open import Categories.Category.Product using (πʳ; πˡ; _※_)
 open import Categories.Category.Construction.Presheaves using (CoPresheaves)
 open import Categories.Category.Construction.Functors using (eval)
-open import Categories.Category.Construction.Functors
+open import Categories.Category.Construction.Functors using (Functors)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Functor.Hom using (module Hom; Hom[_][_,-]; Hom[_][-,-])
@@ -28,15 +27,17 @@ import Categories.Morphism as Mor
 import Categories.Morphism.Reasoning as MR
 import Categories.NaturalTransformation.Hom as NT-Hom
 
+open Func
+
 private
   variable
     o ℓ e : Level
 
 module Yoneda (C : Category o ℓ e) where
   open Category C hiding (op) -- uses lots
-  open HomReasoning using (_○_; ⟺)
+  open HomReasoning using (_○_; ⟺; refl⟩∘⟨_)
   open MR C using (id-comm)
-  open NaturalTransformation using (η; commute)
+  open NaturalTransformation using (η; commute; sym-commute)
   open NT-Hom C using (Hom[C,A]⇒Hom[C,B])
   private
     module CE = Category.Equiv C using (refl)
@@ -56,10 +57,10 @@ module Yoneda (C : Category o ℓ e) where
   yoneda-inverse : (a : Obj) (F : Functor C (Setoids ℓ e)) →
     Inverse (Category.hom-setoid (CoPresheaves C) {Functor.F₀ embed a} {F}) (Functor.F₀ F a)
   yoneda-inverse a F = record
-    { f = λ nat → η nat a ⟨$⟩ id
-    ; f⁻¹ = λ x → ntHelper record
+    { to = λ nat → η nat a ⟨$⟩ id
+    ; from = λ x → ntHelper record
         { η       = λ X → record
-          { _⟨$⟩_ = λ X⇒a → F.₁ X⇒a ⟨$⟩ x
+          { to = λ X⇒a → F.₁ X⇒a ⟨$⟩ x
           ; cong  = λ i≈j → F.F-resp-≈ i≈j SE.refl
           }
         ; commute = λ {X} {Y} X⇒Y {f} {g} f≈g →
@@ -70,19 +71,28 @@ module Yoneda (C : Category o ℓ e) where
              F.₁ X⇒Y ⟨$⟩ (F.₁ g ⟨$⟩ x)
            SR.∎
         }
-    ; cong₁ = λ i≈j → i≈j CE.refl
-    ; cong₂ = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j
-    ; inverse = (λ Fa → F.identity SE.refl) , λ nat {x} {z} {y} z≈y →
-        let module SR     = SetoidR (F.₀ x) in
-        SR.begin
-          F.₁ z ⟨$⟩ (η nat a ⟨$⟩ id) SR.≈˘⟨ commute nat z (CE.refl {a}) ⟩
-          η nat x ⟨$⟩ z ∘ id ∘ id SR.≈⟨ cong (η nat x) (∘-resp-≈ʳ identity² ○ identityʳ ○ z≈y ) ⟩
-          η nat x ⟨$⟩ y
-        SR.∎
+    ; to-cong = λ i≈j → i≈j CE.refl
+    ; from-cong = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j
+    ; inverse =
+       ( λ {b} {nat} eq → 
+          let module SR = SetoidR (F.₀ a) in
+          let open SR in begin
+          to (η nat a) id ≈⟨ eq {a} {id} {id} CE.refl ⟩
+          to (F.₁ id) b    ≈⟨ F.identity (Setoid.refl (F.₀ a) {b}) ⟩
+           b                    ∎)
+       , λ {nat} {y} eq {b} {f} {g} f≈g →
+          let open Setoid (F.₀ b) in
+          let module SR = SetoidR (F.₀ b) in
+          let open SR in
+          begin
+            to (F.₁ f) y                      ≈⟨ cong (F.₁ f) eq ⟩
+            to (F.₁ f) (to (η nat a) id) ≈⟨ sym-commute nat f CE.refl  ⟩
+            to (η nat b) (f ∘ id ∘ id)        ≈⟨ cong (η nat b) (refl⟩∘⟨ identity² ○ (identityʳ ○ f≈g)) ⟩
+            to (η nat b) g                    ∎ 
     }
     where
     module F = Functor F using (₀; ₁; F-resp-≈; homomorphism; identity)
-    module SE = Setoid (F.₀ a) using (refl)
+    module SE = Setoid (F.₀ a)
 
   private
     Nat[Hom[C][c,-],F] : Bifunctor (CoPresheaves C) C (Setoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e))
@@ -100,7 +110,7 @@ module Yoneda (C : Category o ℓ e) where
     { F⇒G = ntHelper record
       { η       = λ where
         (F , A) → record
-          { _⟨$⟩_ = λ α → lift (yoneda-inverse.f α)
+          { to = λ α → lift (yoneda-inverse.to α)
           ; cong  = λ i≈j → lift (i≈j CE.refl)
           }
       ; commute = λ where
@@ -108,15 +118,15 @@ module Yoneda (C : Category o ℓ e) where
       }
     ; F⇐G = ntHelper record
       { η       = λ (F , A) → record
-          { _⟨$⟩_ = λ x → yoneda-inverse.f⁻¹ (lower x)
+          { to = λ x → yoneda-inverse.from (lower x)
           ; cong  = λ i≈j y≈z → Functor.F-resp-≈ F y≈z (lower i≈j)
           }
       ; commute = λ { {F , A} {G , B} (α , f) {X} {Y} eq {Z} {h} {i} eq′ → helper′ α f (lower eq) eq′}
       }
     ; iso = λ (F , A) → record
         { isoˡ = λ {α β} i≈j {X} y≈z →
-          Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.inverseʳ α {x = X} y≈z) (i≈j CE.refl)
-        ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.inverseˡ {F = F} _) (lower eq))
+          Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.strictlyInverseʳ α {x = X} y≈z ) (i≈j CE.refl)
+        ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.strictlyInverseˡ {F = F} _) (lower eq))
         }
     }
     where helper : {F : Functor C (Setoids ℓ e)}
diff --git a/src/Categories/Diagram/Colimit/DualProperties.agda b/src/Categories/Diagram/Colimit/DualProperties.agda
index a987c8c89..de623fabe 100644
--- a/src/Categories/Diagram/Colimit/DualProperties.agda
+++ b/src/Categories/Diagram/Colimit/DualProperties.agda
@@ -6,8 +6,6 @@ open import Categories.Functor hiding (id)
 module Categories.Diagram.Colimit.DualProperties
   {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} where
 
-open import Function.Equality renaming (id to idFun)
-
 open import Categories.Category.Instance.Setoids
 open import Categories.Diagram.Duality C
 open import Categories.Functor.Hom
diff --git a/src/Categories/Enriched/Over/Setoids.agda b/src/Categories/Enriched/Over/Setoids.agda
index a9dc633b8..e7e04ac7b 100644
--- a/src/Categories/Enriched/Over/Setoids.agda
+++ b/src/Categories/Enriched/Over/Setoids.agda
@@ -6,7 +6,7 @@ module Categories.Enriched.Over.Setoids where
 open import Level
 open import Data.Product using (uncurry; proj₁; proj₂; Σ; _,_)
 open import Data.Unit using (tt)
-open import Function.Equality using (_⟨$⟩_; cong)
+open import Function.Bundles using (_⟨$⟩_; Func)
 open import Relation.Binary.Bundles using (Setoid)
 
 open import Categories.Category.Core using () renaming (Category to SCategory)
@@ -30,11 +30,11 @@ Cat→Cat′ C = record
     ; isEquivalence = equiv
     }
   ; id = record
-    { _⟨$⟩_ = λ _ → id
+    { to = λ _ → id
     ; cong = λ _ → Equiv.refl
     }
   ; ⊚ = record
-    { _⟨$⟩_ = uncurry _∘_
+    { to = uncurry _∘_
     ; cong = uncurry ∘-resp-≈
     }
   ; ⊚-assoc = λ { {x = (x₁ , x₂) , x₃} {(y₁ , y₂) , y₃} ((x₁≈y₁ , x₂≈y₂) , x₃≈y₃) → begin
@@ -65,7 +65,7 @@ Cat′→Cat 𝓒 = record
     ; sym = sym (hom A B)
     ; trans = trans (hom A B)
     }
-  ; ∘-resp-≈ = λ f≈h g≈i → cong ⊚ (f≈h , g≈i)
+  ; ∘-resp-≈ = λ f≈h g≈i → Func.cong ⊚ (f≈h , g≈i)
   }
   where
   open Category 𝓒
diff --git a/src/Categories/Functor/Construction/LiftSetoids.agda b/src/Categories/Functor/Construction/LiftSetoids.agda
index 643cd797c..18a5f4cb3 100644
--- a/src/Categories/Functor/Construction/LiftSetoids.agda
+++ b/src/Categories/Functor/Construction/LiftSetoids.agda
@@ -2,14 +2,15 @@
 
 module Categories.Functor.Construction.LiftSetoids where
 
-open import Level
-open import Relation.Binary
-open import Function.Equality
+open import Level using (Level; _⊔_; Lift; lift)
+open import Relation.Binary.Bundles using (Setoid)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Function using (_$_) renaming (id to idf)
 
-open import Categories.Category
-open import Categories.Category.Instance.Setoids
-open import Categories.Functor
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor.Core using (Functor)
+
+open Func
 
 private
   variable
@@ -34,7 +35,7 @@ LiftSetoids : ∀ c′ ℓ′ → Functor (Setoids c ℓ) (Setoids (c ⊔ c′)
 LiftSetoids c′ ℓ′ = record
   { F₀           = LiftedSetoid c′ ℓ′
   ; F₁           = λ f → record
-    { _⟨$⟩_  = λ where (lift x)  → lift $ f ⟨$⟩ x
+    { to    = λ where (lift x)  → lift $ f ⟨$⟩ x
     ; cong  = λ where (lift eq) → lift $ cong f eq
     }
   ; identity     = idf
diff --git a/src/Categories/Functor/Construction/ObjectRestriction.agda b/src/Categories/Functor/Construction/ObjectRestriction.agda
index aa1174b91..816bb3c75 100644
--- a/src/Categories/Functor/Construction/ObjectRestriction.agda
+++ b/src/Categories/Functor/Construction/ObjectRestriction.agda
@@ -4,14 +4,14 @@
 
 module Categories.Functor.Construction.ObjectRestriction where
 
-open import Level
-open import Data.Product using (proj₁)
+open import Level using (Level)
+open import Data.Product using (proj₁; _,_)
 open import Relation.Unary using (Pred)
 open import Function using () renaming (id to id→)
 
-open import Categories.Category.Core
+open import Categories.Category.Core using (Category)
 open import Categories.Category.Construction.ObjectRestriction
-open import Categories.Functor.Core
+open import Categories.Functor.Core using (Functor)
 open import Categories.Functor.Properties using (Faithful; Full)
 
 private
@@ -20,7 +20,7 @@ private
     C : Category o ℓ e
 
 RestrictionFunctor : {ℓ′ : Level} → (C : Category o ℓ e) → (E : Pred (Category.Obj C) ℓ′) → Functor (ObjectRestriction C E) C
-RestrictionFunctor C E = record
+RestrictionFunctor C _ = record
   { F₀ = proj₁
   ; F₁ = id→
   ; identity = Equiv.refl
@@ -31,13 +31,7 @@ RestrictionFunctor C E = record
   open Category C
 
 RF-Faithful : {E : Pred (Category.Obj C) ℓ′} → Faithful (RestrictionFunctor C E)
-RF-Faithful _ _ = id→
+RF-Faithful = id→
 
 RF-Full : {E : Pred (Category.Obj C) ℓ′} → Full (RestrictionFunctor C E)
-RF-Full {C = C} = record
-  { from = record
-    { _⟨$⟩_ = id→
-    ; cong = id→
-    }
-  ; right-inverse-of = λ _ → Category.Equiv.refl C
-  }
+RF-Full {C = C} f = f , Category.Equiv.refl C
diff --git a/src/Categories/Functor/Construction/SubCategory/Properties.agda b/src/Categories/Functor/Construction/SubCategory/Properties.agda
index 2a1f292cc..11e35e6ec 100644
--- a/src/Categories/Functor/Construction/SubCategory/Properties.agda
+++ b/src/Categories/Functor/Construction/SubCategory/Properties.agda
@@ -7,9 +7,10 @@ module Categories.Functor.Construction.SubCategory.Properties {o ℓ e} (C : Cat
 open Category C
 open Equiv
 
+open import Data.Product using (_,_)
 open import Level
-open import Function.Base       using () renaming (id to id→)
-open import Function.Surjection using (Surjection) renaming (id to id↠)
+open import Function.Base    using () renaming (id to id→)
+open import Function.Bundles using (Surjection)
 
 open import Categories.Category.SubCategory C
 open import Categories.Functor.Construction.SubCategory C
@@ -22,10 +23,10 @@ private
     U : I → Obj
 
 SubFaithful : ∀ (sub : SubCat {i} {ℓ′} I) → Faithful (Sub sub)
-SubFaithful _ _ _ = id→
+SubFaithful _ x≈y = x≈y
 
 FullSubFaithful : Faithful (FullSub {U = U})
-FullSubFaithful _ _ = id→
+FullSubFaithful = id→
 
 FullSubFull : Full (FullSub {U = U})
-FullSubFull = Surjection.surjective id↠
+FullSubFull f = f , refl
diff --git a/src/Categories/Functor/Hom.agda b/src/Categories/Functor/Hom.agda
index 703d30fd8..046fabdc4 100644
--- a/src/Categories/Functor/Hom.agda
+++ b/src/Categories/Functor/Hom.agda
@@ -26,8 +26,8 @@ module Hom {o ℓ e} (C : Category o ℓ e) where
     { F₀           = F₀′
     ; F₁           = λ where
       (f , g) → record
-        { _⟨$⟩_ = λ h → g ∘ h ∘ f
-        ; cong  = ∘-resp-≈ʳ ∙ ∘-resp-≈ˡ
+        { to = λ h → g ∘ h ∘ f
+        ; cong = ∘-resp-≈ʳ ∙ ∘-resp-≈ˡ
         }
     ; identity     = identity′
     ; homomorphism = homomorphism′
diff --git a/src/Categories/Functor/Hom/Properties/Contra.agda b/src/Categories/Functor/Hom/Properties/Contra.agda
index 6cc4b3bda..2bca4f0db 100644
--- a/src/Categories/Functor/Hom/Properties/Contra.agda
+++ b/src/Categories/Functor/Hom/Properties/Contra.agda
@@ -8,7 +8,7 @@ private
   module C = Category C
 
 open import Level
-open import Function.Equality renaming (id to idFun)
+open import Function.Construct.Identity using () renaming (function to idFun)
 
 open import Categories.Category.Instance.Setoids
 open import Categories.Diagram.Limit
@@ -44,11 +44,11 @@ module _ (W : Obj) {F : Functor J C} (col : Colimit F) where
     where Hom≃ : Hom[ op ][ W ,-] ≃ Hom[-, W ]
           Hom≃ = record
             { F⇒G = ntHelper record
-              { η       = λ _ → idFun
+              { η       = λ _ → idFun hom-setoid
               ; commute = λ _ eq → C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq) ○ C.assoc
               }
             ; F⇐G = ntHelper record
-              { η       = λ _ → idFun
+              { η       = λ _ → idFun hom-setoid
               ; commute = λ _ eq → C.sym-assoc ○ C.∘-resp-≈ˡ (C.∘-resp-≈ʳ eq)
               }
             ; iso = λ _ → record
diff --git a/src/Categories/Functor/Hom/Properties/Covariant.agda b/src/Categories/Functor/Hom/Properties/Covariant.agda
index 0fb807ccd..3ac32183b 100644
--- a/src/Categories/Functor/Hom/Properties/Covariant.agda
+++ b/src/Categories/Functor/Hom/Properties/Covariant.agda
@@ -4,19 +4,20 @@ open import Categories.Category
 
 module Categories.Functor.Hom.Properties.Covariant {o ℓ e} (C : Category o ℓ e) where
 
-open import Level
-open import Function.Equality using (Π)
+open import Level using (Level)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Relation.Binary using (Setoid)
 
-open import Categories.Category.Construction.Cones
-open import Categories.Category.Instance.Setoids
-open import Categories.Diagram.Cone.Properties
-open import Categories.Diagram.Limit
-open import Categories.Functor
-open import Categories.Functor.Limits
-open import Categories.Functor.Hom
+open import Categories.Category.Construction.Cones using (Cone; Cone⇒; Cones)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Diagram.Cone.Properties using (F-map-Coneˡ)
+open import Categories.Diagram.Limit using (Limit; ψ-≈⇒rep-≈)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Limits using (Continuous)
+open import Categories.Functor.Hom using (module Hom)
 
 import Categories.Morphism.Reasoning as MR
+open Func
 
 private
   variable
@@ -26,7 +27,6 @@ private
 
 open Category C
 open Hom C
-open Π
 
 -- Hom functor preserves limits in C
 module _ (W : Obj) {F : Functor J C} (lim : Limit F) where
@@ -58,21 +58,21 @@ module _ (W : Obj) {F : Functor J C} (lim : Limit F) where
       ! : Cones HomF [ K , ⊤ ]
       ! = record
         { arr     = record
-          { _⟨$⟩_ = λ x → rep (KW x)
+          { to = λ x → rep (KW x)
           ; cong  = λ {x y} eq → ψ-≈⇒rep-≈ F W (Cone.apex (KW x)) (Cone.apex (KW y)) lim
-                                              (λ A → cong (K.ψ A) eq)
+                                              (λ A → Func.cong (K.ψ A) eq)
           }
         ; commute = λ {X} {x y} eq → begin
           proj X ∘ rep (KW x) ∘ C.id ≈⟨ refl⟩∘⟨ C.identityʳ ⟩
           proj X ∘ rep (KW x)        ≈⟨ lim.commute ⟩
-          K.ψ X ⟨$⟩ x                ≈⟨ cong (K.ψ X) eq ⟩
+          K.ψ X ⟨$⟩ x                ≈⟨ Func.cong (K.ψ X) eq ⟩
           K.ψ X ⟨$⟩ y                ∎
         }
 
     !-unique : ∀ {K : Cone HomF} (f : Cones HomF [ K , ⊤ ]) → Cones HomF [ ! K ≈ f ]
     !-unique {K} f {x} {y} x≈y = begin
       rep (KW K x) ≈⟨ terminal.!-unique f′ ⟩
-      f.arr ⟨$⟩ x  ≈⟨ cong f.arr x≈y ⟩
+      f.arr ⟨$⟩ x  ≈⟨ Func.cong f.arr x≈y ⟩
       f.arr ⟨$⟩ y  ∎
       where module K = Cone _ K
             module f = Cone⇒ _ f
diff --git a/src/Categories/Functor/Instance/0-Truncation.agda b/src/Categories/Functor/Instance/0-Truncation.agda
index d7f7554a2..4ad95941f 100644
--- a/src/Categories/Functor/Instance/0-Truncation.agda
+++ b/src/Categories/Functor/Instance/0-Truncation.agda
@@ -8,7 +8,7 @@ module Categories.Functor.Instance.0-Truncation where
 -- Groupoids (see Categories.Functor.Adjoint.Instance.ZeroTruncation)
 
 import Function
-open import Function.Equality using (_⟶_)
+open import Function.Bundles using (Func)
 open import Relation.Binary using (Setoid)
 
 open import Categories.Category using (Category; _[_≈_])
@@ -44,8 +44,8 @@ Trunc {o} {ℓ} {e} = record
        where open Groupoid G
 
      TruncMap : ∀ {G H} → Functor (category G) (category H) →
-                TruncSetoid G ⟶ TruncSetoid H
-     TruncMap F = record { _⟨$⟩_ = F₀ F ; cong  = F₁ F }
+                Func (TruncSetoid G) (TruncSetoid H)
+     TruncMap F = record { to = F₀ F ; cong  = F₁ F }
 
      TruncRespNI : ∀ {G H : Groupoid o ℓ e}
                    {E F : Functor (category G) (category H)} →
diff --git a/src/Categories/Functor/Instance/ConnectedComponents.agda b/src/Categories/Functor/Instance/ConnectedComponents.agda
index 68f0bbe8d..4503124a9 100644
--- a/src/Categories/Functor/Instance/ConnectedComponents.agda
+++ b/src/Categories/Functor/Instance/ConnectedComponents.agda
@@ -17,7 +17,7 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIs
 Π₀ = record
   { F₀ = λ C → ST.setoid (Category._⇒_ C) (Category.id C)
   ; F₁ = λ F → record
-    { _⟨$⟩_ = Functor.F₀ F
+    { to = Functor.F₀ F
     ; cong = ST.gmap (Functor.F₀ F) (Functor.F₁ F)
     }
   ; identity = λ x → x
diff --git a/src/Categories/Functor/Instance/SetoidDiscrete.agda b/src/Categories/Functor/Instance/SetoidDiscrete.agda
index a97d8c675..8aa3e1f6b 100644
--- a/src/Categories/Functor/Instance/SetoidDiscrete.agda
+++ b/src/Categories/Functor/Instance/SetoidDiscrete.agda
@@ -15,7 +15,9 @@ import Categories.Category.Construction.SetoidDiscrete as D
 
 open import Relation.Binary using (Setoid)
 open import Function using () renaming (id to idf; _∘_ to _●_)
-open import Function.Equality using (_⟨$⟩_; _⟶_; cong; _∘_) renaming (id to id⟶)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to id⟶)
+open import Function.Construct.Composition using (function)
 
 Discrete : ∀ {o ℓ e} → Functor (Setoids o ℓ) (Cats o ℓ e)
 Discrete {o} {ℓ} {e} = record
@@ -27,27 +29,27 @@ Discrete {o} {ℓ} {e} = record
    }
    where
      open DiscreteCategory
-     DiscreteFunctor : {A B : Setoid o ℓ} → (A ⟶ B) → Cats o ℓ e [ category (D.Discrete A) , category (D.Discrete B) ]
+     DiscreteFunctor : {A B : Setoid o ℓ} → (Func A B) → Cats o ℓ e [ category (D.Discrete A) , category (D.Discrete B) ]
      DiscreteFunctor f = record
        { F₀ = f ⟨$⟩_
-       ; F₁ = cong f
+       ; F₁ = Func.cong f
        ; identity = _
        ; homomorphism = _
        ; F-resp-≈ = _
        }
-     DiscreteId : {A : Setoid o ℓ} → NaturalIsomorphism (DiscreteFunctor {A} id⟶) id
+     DiscreteId : {A : Setoid o ℓ} → NaturalIsomorphism (DiscreteFunctor {A} (id⟶ A)) id
      DiscreteId {A} = record
        { F⇒G = record { η = λ _ → refl ; commute = _ }
        ; F⇐G = record { η = λ _ → refl ; commute = _ }
        } where open Setoid A
-     PointwiseHom : {X Y Z : Setoid o ℓ} {g : X ⟶ Y} {h : Y ⟶ Z} →
-       NaturalIsomorphism (DiscreteFunctor (h ∘ g)) (DiscreteFunctor h ∘F DiscreteFunctor g)
+     PointwiseHom : {X Y Z : Setoid o ℓ} {g : Func X Y} {h : Func Y Z} →
+       NaturalIsomorphism (DiscreteFunctor (function g h)) (DiscreteFunctor h ∘F DiscreteFunctor g)
      PointwiseHom {_} {_} {Z} = record
        { F⇒G = record { η = λ _ → refl }
        ; F⇐G = record { η = λ _ → refl }
        }
        where open Setoid Z
-     ExtensionalityNI : {A B : Setoid o ℓ} {f g : A ⟶ B} → let open Setoid A in
+     ExtensionalityNI : {A B : Setoid o ℓ} {f g : Func A B} → let open Setoid A in
       ({x y : Carrier} → x ≈ y → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ y)) →
       NaturalIsomorphism (DiscreteFunctor f) (DiscreteFunctor g)
      ExtensionalityNI {A} {B} cong≈ = record
diff --git a/src/Categories/Functor/Power.agda b/src/Categories/Functor/Power.agda
index 3e432b671..5d4cfa5f8 100644
--- a/src/Categories/Functor/Power.agda
+++ b/src/Categories/Functor/Power.agda
@@ -15,7 +15,7 @@ open Equiv
 open import Level using (Level; _⊔_)
 open import Data.Nat.Base using (ℕ; _+_; zero; suc; _<_)
 open import Data.Product using (_,_)
-open import Data.Fin.Base using (Fin; inject+; raise; zero; suc; fromℕ<; splitAt; join)
+open import Data.Fin.Base using (Fin; _↑ˡ_; _↑ʳ_; zero; suc; fromℕ<; splitAt; join)
 open import Data.Sum using (_⊎_; inj₁; inj₂; map) renaming ([_,_] to ⟦_,_⟧; [_,_]′ to ⟦_,_⟧′)
 open import Data.Vec.N-ary hiding (curryⁿ)
 open import Function.Base as Fun using (flip; _$_) renaming (_∘_ to _∙_; id to idf)
@@ -163,7 +163,7 @@ flattenP-assocʳ {n₁} {n₂} {n₃} F = record
   ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs ∙ pack)
   }
   where module F = Functor F
-        pack = ⟦ inject+ n₃ ∙ inject+ n₂ , ⟦ inject+ n₃ ∙ raise n₁ , raise (n₁ + n₂) ⟧′ ⟧′
+        pack = ⟦ (_↑ˡ n₃) ∙ (_↑ˡ n₂) , ⟦ (_↑ˡ n₃) ∙ (n₁ ↑ʳ_) , (n₁ + n₂) ↑ʳ_ ⟧′ ⟧′
 
 reduce2ʳ : ∀ (G : Bifunctor C C C) {n₁ n₂ n₃} (F₁ : Powerendo n₁) (F₂ : Powerendo n₂) (F₃ : Powerendo n₃) → Powerendo ((n₁ + n₂) + n₃)
 reduce2ʳ G F₁ F₂ F₃ = flattenP-assocʳ $ reduce′ G F₁ $ reduce′ G F₂ F₃
@@ -306,7 +306,7 @@ widenˡ l F = record
   ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs ∙ pack)
   }
   where module F = Functor F
-        pack = raise l
+        pack = l ↑ʳ_
 
 widenʳ : ∀ (r : ℕ) (F : Powerendo n) → Powerendo (n + r)
 widenʳ r F = record
@@ -317,4 +317,4 @@ widenʳ r F = record
   ; F-resp-≈     = λ fs≈gs → F.F-resp-≈ (fs≈gs ∙ pack)
   }
   where module F = Functor F
-        pack = inject+ r
+        pack = _↑ˡ r
diff --git a/src/Categories/Functor/Profunctor.agda b/src/Categories/Functor/Profunctor.agda
index a27e2e916..c7aaf14e8 100644
--- a/src/Categories/Functor/Profunctor.agda
+++ b/src/Categories/Functor/Profunctor.agda
@@ -5,7 +5,8 @@ module Categories.Functor.Profunctor where
 open import Level
 open import Data.Product using (_,_; _×_)
 open import Function using () -- renaming (_∘′_ to _∙_)
-open import Function.Equality using (_⟨$⟩_; cong)
+open import Function.Bundles using (_⟨$⟩_; Func)
+open Func using (cong)
 open import Relation.Binary using (Setoid; module Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidR
 
@@ -220,7 +221,7 @@ _▻_ {oC} {ℓC} {eC} {oD} {ℓD} {eD} {oE} {ℓE} {eE} {ℓP} {eP} {ℓQ} {eQ}
       {LiftSetoids (ℓC ⊔ ℓQ) (eC ⊔ eQ) ∘F appʳ P.bimodule d}
       {LiftSetoids (ℓC ⊔ ℓP) (eC ⊔ eP) ∘F appʳ Q.bimodule c}
   ; F₁ = λ (df , cf) → record
-    { _⟨$⟩_ = λ ϕ →
+    { to = λ ϕ →
         (LiftSetoids (ℓC ⊔ ℓP) (eC ⊔ eP) ∘ˡ appʳ-nat Q.bimodule cf)
         ∘ᵥ ϕ
         ∘ᵥ (LiftSetoids (ℓC ⊔ ℓQ) (eC ⊔ eQ) ∘ˡ appʳ-nat P.bimodule df)
@@ -249,7 +250,7 @@ _◅_ {oC} {ℓC} {eC} {oD} {ℓD} {eD} {oE} {ℓE} {eE} {ℓP} {eP} {ℓQ} {eQ}
       {LiftSetoids (ℓE ⊔ ℓP) (eE ⊔ eP) ∘F appˡ Q.bimodule d}
       {LiftSetoids (ℓE ⊔ ℓQ) (eE ⊔ eQ) ∘F appˡ P.bimodule e}
   ; F₁ = λ (ef , df) → record
-    { _⟨$⟩_ = λ ϕ →
+    { to = λ ϕ →
         (LiftSetoids (ℓE ⊔ ℓQ) (eE ⊔ eQ) ∘ˡ appˡ-nat P.bimodule ef)
         ∘ᵥ ϕ
         ∘ᵥ (LiftSetoids (ℓE ⊔ ℓP) (eE ⊔ eP) ∘ˡ appˡ-nat Q.bimodule df)
@@ -287,7 +288,7 @@ module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where
       ; isEquivalence = D.equiv
       }
     ; F₁ = λ (f , g) → record
-      { _⟨$⟩_ = λ x → g ∘ x ∘ F₁ f
+      { to = λ x → g ∘ x ∘ F₁ f
       ; cong  = λ x → begin _ ≈⟨ refl⟩∘⟨ x ⟩∘⟨refl ⟩ _ ∎
       }
     ; identity = λ {x} {y} {y'} y≈y' → begin
@@ -318,7 +319,7 @@ module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where
       ; isEquivalence = D.equiv
       }
     ; F₁ = λ (f , g) → record
-      { _⟨$⟩_ = λ x → F₁ g ∘ x ∘ f
+      { to = λ x → F₁ g ∘ x ∘ f
       ; cong  = λ x → begin _ ≈⟨ refl⟩∘⟨ x ⟩∘⟨refl ⟩ _ ∎
       }
     ; identity = λ {x} {y} {y'} y≈y' → begin
diff --git a/src/Categories/Functor/Profunctor/Cograph.agda b/src/Categories/Functor/Profunctor/Cograph.agda
index 6f4db57a0..5fce62447 100644
--- a/src/Categories/Functor/Profunctor/Cograph.agda
+++ b/src/Categories/Functor/Profunctor/Cograph.agda
@@ -6,13 +6,14 @@ open import Level
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product using (_,_; _×_)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Function.Equality using (_⟨$⟩_; cong)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open Func using (cong)
 open import Relation.Binary using (Setoid; module Setoid)
 
-open import Categories.Category
-open import Categories.Functor hiding (id)
+open import Categories.Category using (Category; _[_,_]; _[_∘_]; _[_≈_])
+open import Categories.Functor using (Functor)
 open import Categories.Functor.Bifunctor.Properties using ([_]-commute)
-open import Categories.Functor.Profunctor
+open import Categories.Functor.Profunctor using (Profunctor)
 
 module _ {o ℓ e o′ ℓ′ e′ ℓ″ e″}
     {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (P : Profunctor ℓ″ e″ C D)
diff --git a/src/Categories/Functor/Profunctor/FormalComposite.agda b/src/Categories/Functor/Profunctor/FormalComposite.agda
index fca5f9b19..ce7df494f 100644
--- a/src/Categories/Functor/Profunctor/FormalComposite.agda
+++ b/src/Categories/Functor/Profunctor/FormalComposite.agda
@@ -2,15 +2,16 @@
 
 module Categories.Functor.Profunctor.FormalComposite where
 
-open import Level
+open import Level using (Level; _⊔_)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Construct.Closure.SymmetricTransitive as ST using (Plus⇔; minimal)
 import Relation.Binary.Reasoning.Setoid as SetoidR
 
-open import Relation.Binary.Bundles
-open import Categories.Category
+open import Categories.Category using (Category; _[_,_]; _[_∘_]; _[_≈_])
 open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Functor hiding (id)
-open import Function.Equality using (Π; _⟨$⟩_; cong)
+open import Categories.Functor.Core using (Functor)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open Func using (cong)
 
 open Setoid renaming (_≈_ to _[[_≈_]])
 
diff --git a/src/Categories/Functor/Properties.agda b/src/Categories/Functor/Properties.agda
index 07df576f6..f11d44777 100644
--- a/src/Categories/Functor/Properties.agda
+++ b/src/Categories/Functor/Properties.agda
@@ -2,17 +2,15 @@
 module Categories.Functor.Properties where
 
 -- Properties valid of all Functors
-open import Level
-open import Data.Product using (proj₁; proj₂; _,_; _×_; Σ)
-open import Function.Surjection using (Surjective)
-open import Function.Equivalence using (Equivalence)
-open import Function.Equality using (Π; _⟶_; _⟨$⟩_; cong)
+open import Level using (Level)
+open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
+open import Function.Base using (_$_)
+open import Function.Definitions using (Injective; StrictlySurjective)
 open import Relation.Binary using (_Preserves_⟶_)
-open import Relation.Nullary
 
-open import Categories.Category
+open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]; module Definitions)
 open import Categories.Category.Construction.Core using (module Shorthands)
-open import Categories.Functor
+open import Categories.Functor.Core using (Functor)
 import Categories.Morphism as Morphism
 import Categories.Morphism.Reasoning as Reas
 open import Categories.Morphism.IsoEquiv as IsoEquiv
@@ -29,17 +27,12 @@ Contravariant : ∀ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → S
 Contravariant C D = Functor (Category.op C) D
 
 Faithful : Functor C D → Set _
-Faithful {C = C} {D = D} F = ∀ {X Y} → (f g : C [ X , Y ]) → D [ F₁ f ≈ F₁ g ] → C [ f ≈ g ]
+Faithful {C = C} {D = D} F = ∀ {X Y} → Injective {A = C [ X , Y ]} (C [_≈_]) (D [_≈_]) F₁
   where open Functor F
 
 Full : Functor C D → Set _
-Full {C = C} {D = D} F = ∀ {X Y} → Surjective {To = D.hom-setoid {F₀ X} {F₀ Y}} G
-  where
-    module C = Category C
-    module D = Category D
-    open Functor F
-    G : ∀ {X Y} → (C.hom-setoid {X} {Y}) ⟶ D.hom-setoid {F₀ X} {F₀ Y}
-    G = record { _⟨$⟩_ = F₁ ; cong = F-resp-≈ }
+Full {C = C} {D = D} F = ∀ {X Y} → StrictlySurjective {A = C [ X , Y ]} (D [_≈_]) F₁
+  where open Functor F
 
 FullyFaithful : Functor C D → Set _
 FullyFaithful F = Full F × Faithful F
@@ -53,7 +46,7 @@ EssentiallySurjective {C = C} {D = D} F = (d : Category.Obj D) → Σ C.Obj (λ
   module C = Category C
 
 Conservative : Functor C D → Set _
-Conservative {C = C} {D = D} F = ∀ {A B} {f : C [ A , B ]} {g : D [ F₀ B , F₀ A ]} → Iso D (F₁ f) g → Σ (C [ B , A ]) (λ h → Iso C f h)
+Conservative {C = C} {D = D} F = ∀ {A B} {f : C [ A , B ]} {g : D [ F₀ B , F₀ A ]} → Iso D (F₁ f) g → Σ (C [ B , A ]) (Iso C f)
   where
     open Functor F
     open Morphism
@@ -62,7 +55,7 @@ Conservative {C = C} {D = D} F = ∀ {A B} {f : C [ A , B ]} {g : D [ F₀ B , F
 
 module _ (F : Functor C D) where
   private
-    module C = Category C using (Obj; _∘_; _⇒_; id; module HomReasoning)
+    module C = Category C
     module D = Category D
     module IsoC = IsoEquiv C
     module IsoD = IsoEquiv D
@@ -124,46 +117,48 @@ module _ (F : Functor C D) where
   EssSurj×Full×Faithful⇒Invertible surj full faith = record
     { F₀ = λ d → proj₁ (surj d)
     ; F₁ = λ {A} {B} f →
-      let (a , sa) = surj A in
-      let (b , sb) = surj B in
-      let module S = Surjective (full {a} {b}) in
-      S.from ⟨$⟩ (_≅_.to sb) ∘ f ∘ (_≅_.from sa)
+      let (a , sa) = surj A
+          (b , sb) = surj B
+      in proj₁ (full (_≅_.to sb ∘ f ∘ _≅_.from sa))
     ; identity = λ {A} →
-      let ff = from full
-          (a , sa) = surj A in begin
-      ff ⟨$⟩ _≅_.to sa ∘ D.id ∘ _≅_.from sa ≈⟨ cong ff (E.refl⟩∘⟨ D.identityˡ) ⟩
-      ff ⟨$⟩ _≅_.to sa ∘ _≅_.from sa        ≈⟨ cong ff (_≅_.isoˡ sa) ⟩
-      ff ⟨$⟩ D.id                           ≈˘⟨ cong ff identity ⟩
-      ff ⟨$⟩ F₁ C.id                        ≈⟨ faith _ _ (right-inverse-of full (F₁ C.id)) ⟩
-      C.id ∎
+      let (a , sa) = surj A
+          (f , p) = full (_≅_.to sa ∘ D.id ∘ _≅_.from sa)
+      in faith $ begin
+        F₁ f                           ≈⟨ p ⟩
+        _≅_.to sa ∘ D.id ∘ _≅_.from sa ≈⟨ refl⟩∘⟨ D.identityˡ ⟩
+        _≅_.to sa ∘ _≅_.from sa        ≈⟨ _≅_.isoˡ sa ⟩
+        D.id                           ≈˘⟨ identity ⟩
+        F₁ C.id                        ∎
     ; homomorphism = λ {X} {Y} {Z} {f} {g} →
-      let
-          (x , sx) = surj X
-          (y , sy) = surj Y
-          (z , sz) = surj Z
-          fsx      = from sx
-          tsz      = to sz
-          ff {T₁} {T₂} = from (full {T₁} {T₂}) in
-      faith _ _ (E.begin
-      F₁ (ff ⟨$⟩ tsz ∘ (g ∘ f) ∘ fsx)                             E.≈⟨ right-inverse-of full _ ⟩
-      (tsz ∘ (g ∘ f) ∘ fsx)                                      E.≈⟨ pullˡ (E.refl⟩∘⟨ (E.refl⟩∘⟨ introˡ (isoʳ sy))) ⟩
-      (tsz ∘ g ∘ ((from sy ∘ to sy) ∘ f)) ∘ fsx                  E.≈⟨ pushʳ (E.refl⟩∘⟨ D.assoc) E.⟩∘⟨refl ⟩
-      ((tsz ∘ g) ∘ (from sy ∘ (to sy ∘ f))) ∘ fsx                E.≈⟨ D.sym-assoc E.⟩∘⟨refl ⟩
-      (((tsz ∘ g) ∘ from sy) ∘ (to sy ∘ f)) ∘ fsx                E.≈⟨ D.assoc ⟩
-      ((tsz ∘ g) ∘ from sy) ∘ ((to sy ∘ f) ∘ fsx)                E.≈⟨ D.assoc E.⟩∘⟨ D.assoc  ⟩
-      (tsz ∘ g ∘ from sy) ∘ (to sy ∘ f ∘ fsx)                    E.≈˘⟨ right-inverse-of full _ E.⟩∘⟨ right-inverse-of full _ ⟩
-      F₁ (ff ⟨$⟩ tsz ∘ g ∘ from sy) ∘ F₁ (ff ⟨$⟩ to sy ∘ f ∘ fsx)  E.≈˘⟨ homomorphism ⟩
-      F₁ ((ff ⟨$⟩ tsz ∘ g ∘ from sy) C.∘ (ff ⟨$⟩ to sy ∘ f ∘ fsx)) E.∎)
-    ; F-resp-≈ = λ f≈g → cong (from full) (D.∘-resp-≈ʳ (D.∘-resp-≈ˡ f≈g))
+      let (a , sa) = surj X
+          (b , sb) = surj Y
+          (c , sc) = surj Z
+          (⟨g∘f⟩ , p) = full (_≅_.to sc ∘ (g ∘ f) ∘ _≅_.from sa)
+          (⟨f⟩ , q) = full (_≅_.to sb ∘ f ∘ _≅_.from sa)
+          (⟨g⟩ , r) = full (_≅_.to sc ∘ g ∘ _≅_.from sb)
+      in faith $ begin
+        F₁ ⟨g∘f⟩                                                         ≈⟨ p ⟩
+        _≅_.to sc ∘ (g ∘ f) ∘ _≅_.from sa                               ≈⟨ assoc²'' ⟩
+        (_≅_.to sc ∘ g) ∘ (f ∘ _≅_.from sa)                             ≈⟨ insertInner (_≅_.isoʳ sb) ⟩
+        ((_≅_.to sc ∘ g) ∘ _≅_.from sb) ∘ (_≅_.to sb ∘ f ∘ _≅_.from sa) ≈⟨ D.assoc ⟩∘⟨refl ⟩
+        (_≅_.to sc ∘ g ∘ _≅_.from sb) ∘ (_≅_.to sb ∘ f ∘ _≅_.from sa)   ≈˘⟨ (r ⟩∘⟨ q ) ⟩
+        F₁ ⟨g⟩ ∘ F₁ ⟨f⟩                                                   ≈˘⟨ homomorphism ⟩
+        F₁ (⟨g⟩ C.∘ ⟨f⟩)                                                  ∎
+    ; F-resp-≈ = λ {X} {Y} {f} {g} f≈g →
+      let sa = proj₂ (surj X)
+          sb = proj₂ (surj Y)
+          (⟨f⟩ , p) = full (_≅_.to sb ∘ f ∘ _≅_.from sa)
+          (⟨g⟩ , q) = full (_≅_.to sb ∘ g ∘ _≅_.from sa)
+      in faith $ begin
+        F₁ ⟨f⟩                      ≈⟨ p ⟩
+        _≅_.to sb ∘ f ∘ _≅_.from sa ≈⟨ refl⟩∘⟨ f≈g ⟩∘⟨refl ⟩
+        _≅_.to sb ∘ g ∘ _≅_.from sa ≈˘⟨ q ⟩
+        F₁ ⟨g⟩                      ∎
     }
     where
-    open Morphism._≅_
-    open Morphism D
-    open Reas D
-    open Category D
-    open Surjective
-    open C.HomReasoning
-    module E = D.HomReasoning
+      open Category D
+      open D.HomReasoning
+      open Reas D
 
 -- Functor Composition is Associative and the unit laws are found in
 -- NaturalTransformation.NaturalIsomorphism, reified as associator, unitorˡ and unitorʳ.
diff --git a/src/Categories/Multi/Category/Indexed.agda b/src/Categories/Multi/Category/Indexed.agda
index f6cffc0fe..8c1e99bb3 100644
--- a/src/Categories/Multi/Category/Indexed.agda
+++ b/src/Categories/Multi/Category/Indexed.agda
@@ -10,11 +10,10 @@ open import Data.Product.Properties
 open import Data.Unit.Polymorphic using (⊤; tt)
 open import Data.Vec.Functional
 open import Function.Base using (const) renaming (_∘_ to _●_; id to id→)
-open import Function.Equality using (_⟨$⟩_)
--- note how this is Function.Inverse instead of the one from Function.
-open import Function.Inverse as Inv renaming (id to id↔; _∘_ to trans)
+open import Function.Bundles using (_⟨$⟩_; _↔_; mk↔ₛ′; Inverse)
+open import Function.Construct.Identity renaming (inverse to id↔)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; setoid)
 
 -- any point can be lifted to a function from ⊤
 pointed : {s t : Level} {S : Set s} (x : S) → ⊤ {t} → S
@@ -22,17 +21,17 @@ pointed x _ = x
 
 -- the standard library doesn't seem to have the 'right' version of these.
 ⊤×K↔K : {t k : Level} {K : Set k} → (⊤ {t} × K) ↔ K
-⊤×K↔K = inverse proj₂ (tt ,_) (λ _ → refl) λ _ → refl
+⊤×K↔K = mk↔ₛ′ proj₂ (tt ,_) (λ _ → refl) λ _ → refl
 
 K×⊤↔K : {t k : Level} {K : Set k} → (K × ⊤ {t}) ↔ K
-K×⊤↔K = inverse proj₁ (_, tt) (λ _ → refl) λ _ → refl
+K×⊤↔K = mk↔ₛ′ proj₁ (_, tt) (λ _ → refl) λ _ → refl
 
 ⊤×⊤↔⊤ : {t : Level} → (⊤ {t} × ⊤) ↔ ⊤
-⊤×⊤↔⊤ = inverse proj₁ (λ x → x , x) (λ _ → refl) λ _ → refl
+⊤×⊤↔⊤ = mk↔ₛ′ proj₁ (λ x → x , x) (λ _ → refl) λ _ → refl
 
 Σ-assoc : {a b c : Level} {I : Set a} {J : I → Set b} {K : Σ I J → Set c} →
   Σ (Σ I J) K ↔ Σ I (λ i → Σ (J i) (curry K i))
-Σ-assoc {I = I} {J} {K} = inverse g f (λ _ → refl) λ _ → refl
+Σ-assoc {I = I} {J} {K} = mk↔ₛ′ g f (λ _ → refl) λ _ → refl
   where
   f : Σ I (λ i → Σ (J i) (λ j → K (i , j))) → Σ (Σ I J) K
   f (i , j , k) = (i , j) , k
@@ -68,7 +67,7 @@ record MultiCategory (o ℓ e ı : Level) : Set (suc (o ⊔ ℓ ⊔ e ⊔ ı)) w
           {v : (i : I) → J i → Obj} →
           Hom {I} aₙ a → ((i : I) → Hom (v i) (aₙ i)) → Hom {Σ I J} (uncurry v) a
     _≈[_]_ : {I J : Set ı} {aₙ : I → Obj} {a : Obj} →
-          Hom {I} aₙ a → (σ : I ↔ J) → Hom {J} (aₙ ● ( Inverse.from σ ⟨$⟩_ )) a → Set e
+          Hom {I} aₙ a → (σ : I ↔ J) → Hom {J} (aₙ ● Inverse.from σ) a → Set e
 
     identityˡ : {K : Set ı} {aₖ : K → Obj} {a : Obj} {f : Hom aₖ a} →
               id a ∘ pointed f ≈[ ⊤×K↔K ]  f
@@ -93,14 +92,15 @@ record MultiCategory (o ℓ e ı : Level) : Set (suc (o ⊔ ℓ ⊔ e ⊔ ı)) w
     -- we also need that _≈[_]_ is, in an appropriate sense, an equivalence relation, which in this case
     -- means that _≈[ id↔ ]_ is.  In other words, we don't care when transport is over 'something else'.
     refl≈ : {I : Set ı} {aₙ : I → Obj} {a : Obj} →
-            {h : Hom {I} aₙ a} → h ≈[ id↔ ] h
+            {h : Hom {I} aₙ a} → h ≈[ id↔ (setoid I) ] h
     sym≈ : {I : Set ı} {aₙ : I → Obj} {a : Obj} →
-           {g h : Hom {I} aₙ a} → g ≈[ id↔ ] h → h ≈[ id↔ ] g
+           {g h : Hom {I} aₙ a} → g ≈[ id↔ (setoid I) ] h → h ≈[ id↔ (setoid I) ] g
     trans≈ : {I : Set ı} {aₙ : I → Obj} {a : Obj} →
-           {f g h : Hom {I} aₙ a} → f ≈[ id↔ ] g → g ≈[ id↔ ] h → f ≈[ id↔ ] h
+           {f g h : Hom {I} aₙ a} → f ≈[ id↔ (setoid I) ] g → g ≈[ id↔ (setoid I) ] h → f ≈[ id↔ (setoid I) ] h
 
     ∘-resp-≈ : {I : Set ı} {J : I → Set ı}
                {a : Obj} {aᵢ : I → Obj} {aᵢⱼ : (i : I) → J i → Obj}
                {g g′ : Hom aᵢ a} {f f′ : (i : I) → Hom (aᵢⱼ i) (aᵢ i)} →
-               g ≈[ id↔ ] g′ → (∀ i → f i ≈[ id↔ ] f′ i) →
-               g ∘ f ≈[ id↔ ] g′ ∘ f′
+               g ≈[ id↔ (setoid I) ] g′ → (∀ i → f i ≈[ id↔ (setoid (J i)) ] f′ i) →
+               g ∘ f ≈[ id↔ (setoid (Σ I J)) ] g′ ∘ f′
+
diff --git a/src/Categories/NaturalTransformation/Hom.agda b/src/Categories/NaturalTransformation/Hom.agda
index 0a5111fe0..a875579e4 100644
--- a/src/Categories/NaturalTransformation/Hom.agda
+++ b/src/Categories/NaturalTransformation/Hom.agda
@@ -20,7 +20,7 @@ private
 
 Hom[A,C]⇒Hom[B,C] : {A B : Obj} → (A ⇒ B) → NaturalTransformation Hom[ C ][-, A ] Hom[ C ][-, B ]
 Hom[A,C]⇒Hom[B,C] {A} A⇒B = ntHelper record
-  { η       = λ X → record { _⟨$⟩_ = λ X⇒A → A⇒B ∘ X⇒A ; cong = ∘-resp-≈ʳ }
+  { η       = λ X → record { to = λ X⇒A → A⇒B ∘ X⇒A ; cong = ∘-resp-≈ʳ }
   ; commute = λ f {g} {h} g≈h → begin
       A⇒B ∘ id ∘ g ∘ f   ≈⟨ sym-assoc ⟩
       (A⇒B ∘ id) ∘ g ∘ f ≈⟨ id-comm ⟩∘⟨ g≈h ⟩∘⟨refl ⟩
@@ -30,7 +30,7 @@ Hom[A,C]⇒Hom[B,C] {A} A⇒B = ntHelper record
 
 Hom[C,A]⇒Hom[C,B] : {A B : Obj} → (B ⇒ A) → NaturalTransformation Hom[ C ][ A ,-] Hom[ C ][ B ,-]
 Hom[C,A]⇒Hom[C,B] {A} B⇒A = ntHelper record
-  { η = λ X → record { _⟨$⟩_ = λ A⇒X → A⇒X ∘ B⇒A ; cong = ∘-resp-≈ˡ }
+  { η = λ X → record { to = λ A⇒X → A⇒X ∘ B⇒A ; cong = ∘-resp-≈ˡ }
   ; commute = λ f {g} {h} g≈h → begin
       (f ∘ g ∘ id) ∘ B⇒A ≈⟨ pullʳ assoc ⟩
       f ∘ g ∘ id ∘ B⇒A   ≈⟨ (refl⟩∘⟨ g≈h ⟩∘⟨ id-comm-sym) ⟩
diff --git a/src/Categories/NaturalTransformation/Properties.agda b/src/Categories/NaturalTransformation/Properties.agda
index fd3877862..e949043e8 100644
--- a/src/Categories/NaturalTransformation/Properties.agda
+++ b/src/Categories/NaturalTransformation/Properties.agda
@@ -4,7 +4,7 @@ module Categories.NaturalTransformation.Properties where
 
 open import Level
 open import Data.Product using (Σ; _,_)
-open import Function.Equality using (Π)
+open import Function.Bundles using (Func)
 
 open import Categories.Category
 open import Categories.Category.Product
@@ -100,12 +100,12 @@ module _ {F G : Bifunctor C D E} (α : NaturalTransformation F G) where
 -- unlift universe level
 module _ {c ℓ ℓ′ e} {F G : Functor C (Setoids c ℓ)} (α : NaturalTransformation (LiftSetoids ℓ′ e ∘F F) (LiftSetoids ℓ′ e ∘F G)) where
   open NaturalTransformation α
-  open Π
+  open Func
 
   unlift-nat : NaturalTransformation F G
   unlift-nat = ntHelper record
     { η       = λ X → record
-      { _⟨$⟩_ = λ x → lower (η X ⟨$⟩ lift x)
+      { to = λ x → lower (to (η X) (lift x))
       ; cong = λ eq → lower (cong (η X) (lift eq))
       }
     ; commute = λ f eq → lower (commute f (lift eq))
diff --git a/src/Categories/Tactic/Category.agda b/src/Categories/Tactic/Category.agda
index 1ab24c52b..45690f5e9 100644
--- a/src/Categories/Tactic/Category.agda
+++ b/src/Categories/Tactic/Category.agda
@@ -19,9 +19,9 @@ open import Data.List    as List    using (List; _∷_; [])
 open import Data.Product as Product using (_×_; _,_)
 
 open import Agda.Builtin.Reflection
-open import Reflection.Argument
-open import Reflection.Term using (getName; _⋯⟅∷⟆_)
-open import Reflection.TypeChecking.Monad.Syntax
+open import Reflection.AST.Argument
+open import Reflection.AST.Term using (getName; _⋯⟅∷⟆_)
+open import Reflection.TCM.Syntax
 
 module _ {o ℓ e} (𝒞 : Category o ℓ e) where
 
diff --git a/src/Categories/Yoneda.agda b/src/Categories/Yoneda.agda
index 529750672..6dd4af653 100644
--- a/src/Categories/Yoneda.agda
+++ b/src/Categories/Yoneda.agda
@@ -11,8 +11,7 @@ module Categories.Yoneda where
 --   as Setoids. In addition, Yoneda (yoneda) also says that this isomorphism is natural in a and F.
 open import Level
 open import Function.Base using (_$_)
-open import Function.Bundles using (Inverse)
-open import Function.Equality using (Π; _⟨$⟩_; cong)
+open import Function.Bundles using (Func; Inverse; _⟨$⟩_)
 open import Relation.Binary.Bundles using (module Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidR
 open import Data.Product using (_,_; Σ)
@@ -34,6 +33,8 @@ import Categories.Morphism as Mor
 import Categories.Morphism.Reasoning as MR
 import Categories.NaturalTransformation.Hom as NT-Hom
 
+open Func
+
 private
   variable
     o ℓ e : Level
@@ -42,7 +43,7 @@ module Yoneda (C : Category o ℓ e) where
   open Category C hiding (op) -- uses lots
   open HomReasoning using (_○_; ⟺)
   open MR C using (id-comm)
-  open NaturalTransformation using (η; commute)
+  open NaturalTransformation using (η; commute; sym-commute)
   open NT-Hom C using (Hom[A,C]⇒Hom[B,C])
   private
     module CE = Category.Equiv C using (refl)
@@ -62,10 +63,10 @@ module Yoneda (C : Category o ℓ e) where
   yoneda-inverse : (a : Obj) (F : Presheaf C (Setoids ℓ e)) →
     Inverse (Category.hom-setoid (Presheaves C) {Functor.F₀ embed a} {F}) (Functor.F₀ F a)
   yoneda-inverse a F = record
-    { f = λ nat → η nat a ⟨$⟩ id
-    ; f⁻¹ = λ x → ntHelper record
+    { to = λ nat → η nat a ⟨$⟩ id
+    ; from = λ x → ntHelper record
         { η       = λ X → record
-          { _⟨$⟩_ = λ X⇒a → F.₁ X⇒a ⟨$⟩ x
+          { to = λ X⇒a → F.₁ X⇒a ⟨$⟩ x
           ; cong  = λ i≈j → F.F-resp-≈ i≈j SE.refl
           }
         ; commute = λ {X} {Y} Y⇒X {f} {g} f≈g →
@@ -76,12 +77,18 @@ module Yoneda (C : Category o ℓ e) where
              F.₁ Y⇒X ⟨$⟩ (F.₁ g ⟨$⟩ x)
            SR.∎
         }
-    ; cong₁ = λ i≈j → i≈j CE.refl
-    ; cong₂ = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j
-    ; inverse = (λ Fa → F.identity SE.refl) , λ nat {x} {z} z≈y →
-        let module S     = Setoid (F.₀ x) in
-        S.trans (S.sym (commute nat z CE.refl))
-                (cong (η nat x) (identityˡ ○ identityˡ ○ z≈y))
+    ; to-cong = λ i≈j → i≈j CE.refl
+    ; from-cong = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j
+    ; inverse = record
+      { fst = λ p → Setoid.trans (F.₀ a) (p CE.refl) (F.identity SE.refl)
+      ; snd = λ {nat} p {x} {f} {g} f≈g →
+        let module S = Setoid (F.₀ x) in
+        S.trans
+          (S.trans
+            (cong (F.₁ f) p)
+            (sym-commute nat f CE.refl))
+          (cong (η nat x) (identityˡ ○ identityˡ ○ f≈g))
+      }
     }
     where
     module F = Functor F using (₀; ₁; F-resp-≈; homomorphism; identity)
@@ -107,7 +114,7 @@ module Yoneda (C : Category o ℓ e) where
     { F⇒G = ntHelper record
       { η       = λ where
         (F , A) → record
-          { _⟨$⟩_ = λ α → lift (yoneda-inverse.f α)
+          { to = λ α → lift (yoneda-inverse.to α)
           ; cong  = λ i≈j → lift (i≈j CE.refl)
           }
       ; commute = λ where
@@ -115,15 +122,15 @@ module Yoneda (C : Category o ℓ e) where
       }
     ; F⇐G = ntHelper record
       { η       = λ (F , A) → record
-          { _⟨$⟩_ = λ x → yoneda-inverse.f⁻¹ (lower x)
+          { to = λ x → yoneda-inverse.from (lower x)
           ; cong  = λ i≈j y≈z → Functor.F-resp-≈ F y≈z (lower i≈j)
           }
       ; commute = λ (α , f) eq eq′ → helper′ α f (lower eq) eq′
       }
     ; iso = λ (F , A) → record
         { isoˡ = λ {α β} i≈j {X} y≈z →
-          Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.inverseʳ α {x = X} y≈z) (i≈j CE.refl)
-        ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.inverseˡ {F = F} _) (lower eq))
+          Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.strictlyInverseʳ α {x = X} y≈z) (i≈j CE.refl)
+        ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.strictlyInverseˡ {F = F} _) (lower eq))
         }
     }
     where helper : {F : Functor C.op (Setoids ℓ e)}
@@ -132,8 +139,8 @@ module Yoneda (C : Category o ℓ e) where
                    Setoid._≈_ (Functor.F₀ Nat[Hom[C][-,c],F] (F , A)) β γ →
                    Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ f ∘ id) (Functor.F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id))
           helper {F} {A} {B} f β γ β≈γ = S.begin
-            η β B ⟨$⟩ f ∘ id          S.≈⟨ cong (η β B) (id-comm ○ (⟺ identityˡ)) ⟩
-            η β B ⟨$⟩ id ∘ id ∘ f     S.≈⟨ commute β f CE.refl ⟩
+            η β B ⟨$⟩ f ∘ id         S.≈⟨ cong (η β B) (id-comm ○ (⟺ identityˡ)) ⟩
+            η β B ⟨$⟩ id ∘ id ∘ f    S.≈⟨ commute β f CE.refl ⟩
             F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F.₁ f) (β≈γ CE.refl) ⟩
             F.₁ f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎
             where
@@ -154,7 +161,7 @@ module Yoneda (C : Category o ℓ e) where
             G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h (S′.sym (cong (F.₁ f) eq)) ⟩
             η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈⟨ cong (η α Z) (F.F-resp-≈ eq′ S′.refl) ⟩
             η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) (F.homomorphism (Setoid.refl (F.₀ A))) ⟩
-            η α Z ⟨$⟩ (F.₁ (f ∘ i) ⟨$⟩ Y)        S.∎
+            η α Z ⟨$⟩ (F.₁ (f ∘ i) ⟨$⟩ Y)       S.∎
             where
               module F = Functor F using (₀; ₁; homomorphism; F-resp-≈)
               module G = Functor G using (₀; ₁)
diff --git a/src/Categories/Yoneda/Continuous.agda b/src/Categories/Yoneda/Continuous.agda
index 1fc9415f5..56bdcee41 100644
--- a/src/Categories/Yoneda/Continuous.agda
+++ b/src/Categories/Yoneda/Continuous.agda
@@ -4,7 +4,7 @@ open import Categories.Category
 
 module Categories.Yoneda.Continuous {o ℓ e} (C : Category o ℓ e) where
 
-open import Function.Equality using (Π)
+open import Function.Bundles using (Func; _⟨$⟩_)
 open import Relation.Binary using (Setoid)
 
 open import Categories.Category.Construction.Cones
@@ -22,7 +22,6 @@ import Categories.Morphism.Reasoning as MR
 
 open Hom C
 open Yoneda C
-open Π using (_⟨$⟩_)
 
 private
   module C = Category C
@@ -74,7 +73,7 @@ module _ {o′ ℓ′ e′} {J : Category o′ ℓ′ e′} {F : Functor J C} (L
               K.ψ.η j Y ⟨$⟩ (K.N.₁ f ⟨$⟩ x)       ∎
             }
           }
-        ; commute = λ eq → L.commute ○ Π.cong (K.ψ.η _ _) eq
+        ; commute = λ eq → L.commute ○ Func.cong (K.ψ.η _ _) eq
         }
 
       module _ (f : Cones yF [ K , ⊤ ]) where
diff --git a/src/Categories/Yoneda/Properties.agda b/src/Categories/Yoneda/Properties.agda
index b33ccec73..2229b9537 100644
--- a/src/Categories/Yoneda/Properties.agda
+++ b/src/Categories/Yoneda/Properties.agda
@@ -8,25 +8,20 @@ open import Categories.Category using (Category; _[_,_])
 module Categories.Yoneda.Properties {o ℓ e : Level} (C : Category o ℓ e) where
 
 open import Function.Base using (_$_)
-open import Function.Bundles using (Inverse)
-open import Function.Equality using (Π; _⟨$⟩_; cong)
+open import Function.Bundles using (Func; Inverse; _⟨$⟩_)
 open import Relation.Binary.Bundles using (module Setoid)
 import Relation.Binary.Reasoning.Setoid as SetoidR
 open import Data.Product using (_,_; Σ)
 
-open import Categories.Category.Product
-open import Categories.Category.Construction.Presheaves
-open import Categories.Category.Construction.Functors
-open import Categories.Category.Instance.Setoids
-open import Categories.Functor renaming (id to idF)
+open import Categories.Category.Product using (_⁂_)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Functor.Properties using (Full; Faithful; FullyFaithful)
 open import Categories.Functor.Hom using (module Hom; Hom[_][-,_]; Hom[_][-,-])
-open import Categories.Functor.Bifunctor
-open import Categories.Functor.Presheaf
-open import Categories.Functor.Construction.LiftSetoids
+open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
-open import Categories.Yoneda
+open import Categories.Yoneda using (module Yoneda)
 
 import Categories.Morphism as Mor
 import Categories.Morphism.Reasoning as MR
@@ -34,27 +29,24 @@ import Categories.NaturalTransformation.Hom as NT-Hom
 
 open Category C using (module HomReasoning; id; _∘_; identityˡ; identityʳ; Obj; ∘-resp-≈ˡ; ∘-resp-≈ʳ)
 open HomReasoning
-open NaturalTransformation using (η; commute)
+open NaturalTransformation
 open Yoneda C using (embed; yoneda-inverse; module yoneda)
 private
   module CE = Category.Equiv C using (refl)
   module C = Category C using (op; id)
 
 YoFull : Full embed
-YoFull {X} {Y} = record
-  { from             = record { _⟨$⟩_ = λ ε → η ε X ⟨$⟩ id ; cong = λ i≈j → i≈j CE.refl }
-  ; right-inverse-of = λ ε {x} {z} {y} z≈y →
-    begin
-      (η ε X ⟨$⟩ id) ∘ z      ≈˘⟨ identityˡ ⟩
-      id ∘ (η ε X ⟨$⟩ id) ∘ z ≈˘⟨ commute ε z CE.refl ⟩
-      η ε x ⟨$⟩ id ∘ id ∘ z   ≈⟨ cong (η ε x) (identityˡ ○ identityˡ ○ z≈y) ⟩
-      η ε x ⟨$⟩ y             ∎
-  }
+YoFull {X} {Y} ε = Func.to (η ε X) id , λ {A} {x} {y} x≈y → begin
+  Func.to (η ε X) id ∘ x        ≈⟨ refl⟩∘⟨ x≈y ⟩
+  Func.to (η ε X) id ∘ y        ≈˘⟨ identityˡ ⟩
+  id ∘ Func.to (η ε X) id ∘ y   ≈⟨ sym-commute ε y CE.refl ⟩
+  Func.to (η ε A) (id ∘ id ∘ y) ≈⟨ Func.cong (η ε A) (identityˡ ○ identityˡ) ⟩
+  Func.to (η ε A) y             ∎
 
 YoFaithful : Faithful embed
-YoFaithful f g pres-≈ = begin
+YoFaithful {X} {Y} {f} {g} p = begin
   f      ≈˘⟨ identityʳ ⟩
-  f ∘ id ≈⟨ pres-≈ CE.refl ⟩
+  f ∘ id ≈⟨ p CE.refl ⟩
   g ∘ id ≈⟨ identityʳ ⟩
   g      ∎
 
@@ -69,24 +61,23 @@ yoneda-iso {A} {B} niso = record
   ; to   = ⇐.η B ⟨$⟩ id
   ; iso  = record
     { isoˡ = begin
-      (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
-      id ∘ (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id) ≈⟨  B⇒A.inverseʳ F⇐G CE.refl  ⟩
-      ⇐.η A ⟨$⟩ (⇒.η A ⟨$⟩ id)             ≈⟨ isoX.isoˡ CE.refl ⟩
-      id                                   ∎
+      (⇐.η B ⟨$⟩ id) ∘ (⇒.η A ⟨$⟩ id)                ≈˘⟨ identityˡ ⟩
+      C.id ∘ Func.to (⇐.η B) id ∘ Func.to (⇒.η A) id ≈⟨ B⇒A.strictlyInverseʳ F⇐G CE.refl ⟩
+      Func.to (⇐.η A) (Func.to (⇒.η A) id)           ≈⟨ iso.isoˡ A CE.refl ⟩
+      id                                             ∎
     ; isoʳ = begin
-      (⇒.η A ⟨$⟩ id) ∘ (⇐.η B ⟨$⟩ id)      ≈˘⟨ identityˡ ⟩
-      id ∘ (⇒.η A ⟨$⟩ id) ∘ (⇐.η B ⟨$⟩ id) ≈⟨  A⇒B.inverseʳ F⇒G CE.refl ⟩
-      ⇒.η B ⟨$⟩ (⇐.η B ⟨$⟩ id)             ≈⟨ isoX.isoʳ CE.refl ⟩
-      id                                   ∎
+      Func.to (⇒.η A) C.id ∘ Func.to (⇐.η B) C.id      ≈˘⟨ identityˡ ⟩
+      C.id ∘ Func.to (⇒.η A) id ∘ Func.to (⇐.η B) C.id ≈⟨ A⇒B.strictlyInverseʳ F⇒G CE.refl ⟩
+      Func.to (⇒.η B) (Func.to (⇐.η B) id)             ≈⟨ iso.isoʳ B CE.refl ⟩
+      id ∎
     }
   }
   where
-  open NaturalIsomorphism niso
-  A⇒B = yoneda-inverse A (Functor.F₀ embed B)
-  B⇒A = yoneda-inverse B (Functor.F₀ embed A)
-  module A⇒B = Inverse A⇒B using (inverseʳ)
-  module B⇒A = Inverse B⇒A using (inverseʳ)
-  module isoX {X} = Mor.Iso (iso X) using (isoʳ; isoˡ)
+    open NaturalIsomorphism niso
+    A⇒B = yoneda-inverse A (Functor.F₀ embed B)
+    B⇒A = yoneda-inverse B (Functor.F₀ embed A)
+    module A⇒B = Inverse A⇒B
+    module B⇒A = Inverse B⇒A
 
 module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where
   private
@@ -106,7 +97,7 @@ module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where
                        NaturalTransformation Hom[ C ][-, F.₀ X ] Hom[ C ][-, G.₀ X ]
       nat-appʳ X α = ntHelper record
         { η       = λ Y → η α (Y , X)
-        ; commute = λ {_ Y} f eq → cong (η α (Y , X)) (∘-resp-≈ˡ (⟺ F.identity)) ○ commute α (f , D.id) eq ○ ∘-resp-≈ˡ G.identity
+        ; commute = λ {_ Y} f eq → Func.cong (η α (Y , X)) (∘-resp-≈ˡ (⟺ F.identity)) ○ commute α (f , D.id) eq ○ ∘-resp-≈ˡ G.identity
         }
 
       transform : NaturalTransformation Hom[-,F-] Hom[-,G-] → NaturalTransformation F G
@@ -114,8 +105,8 @@ module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where
         { η       = λ X → η α (F.₀ X , X) ⟨$⟩ id
         ; commute = λ {X Y} f → begin
           (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f       ≈˘⟨ identityˡ ⟩
-          id ∘ (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f  ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, G.₀ Y ] , _} (idN , F.₁ f) {nat-appʳ Y α} {nat-appʳ Y α} (cong (η α _))) ⟩
-          η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id         ≈⟨ cong (η α (F.₀ X , Y)) (∘-resp-≈ʳ (⟺ identityˡ)) ⟩
+          id ∘ (η α (F.₀ Y , Y) ⟨$⟩ id) ∘ F.₁ f  ≈˘⟨ lower (yoneda.⇒.commute {Y = Hom[ C ][-, G.₀ Y ] , _} (idN , F.₁ f) {nat-appʳ Y α} {nat-appʳ Y α} (Func.cong (η α _))) ⟩
+          η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id         ≈⟨ Func.cong (η α (F.₀ X , Y)) (∘-resp-≈ʳ (⟺ identityˡ)) ⟩
           η α (F.₀ X , Y) ⟨$⟩ F.₁ f ∘ id ∘ id    ≈⟨ commute α (id , f) CE.refl ⟩
           G.₁ f ∘ (η α (F.₀ X , X) ⟨$⟩ id) ∘ id  ≈⟨ refl⟩∘⟨ identityʳ ⟩
           G.₁ f ∘ (η α (F.₀ X , X) ⟨$⟩ id)      ∎
@@ -145,8 +136,8 @@ module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where
                                                                                   (idN , (⇒.η (F.₀ X , X) ⟨$⟩ id))
                                                                                   {nat-appʳ {F = G} {F} X F⇐G}
                                                                                   {nat-appʳ {F = G} {F} X F⇐G}
-                                                                                  (cong (⇐.η (_ , X) ))) ⟩
-          ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ cong (⇐.η _) identityʳ ⟩
+                                                                                  (Func.cong (⇐.η (_ , X) ))) ⟩
+          ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ Func.cong (⇐.η _) identityʳ ⟩
           ⇐.η (F.₀ X , X) ⟨$⟩ (⇒.η (F.₀ X , X) ⟨$⟩ id)             ≈⟨ iso.isoˡ _ CE.refl ⟩
           id                                                  ∎
         ; isoʳ = begin
@@ -155,8 +146,8 @@ module _ {o′ ℓ′ e′} {D : Category o′ ℓ′ e′} where
                                                                                    (idN , (⇐.η (G.₀ X , X) ⟨$⟩ C.id))
                                                                                    {nat-appʳ {F = F} {G} X F⇒G}
                                                                                    {nat-appʳ {F = F} {G} X F⇒G}
-                                                                                   (cong (⇒.η _))) ⟩
-          ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ cong (⇒.η _) identityʳ ⟩
+                                                                                   (Func.cong (⇒.η _))) ⟩
+          ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id) ∘ id        ≈⟨ Func.cong (⇒.η _) identityʳ ⟩
           ⇒.η (G.₀ X , X) ⟨$⟩ (⇐.η (G.₀ X , X) ⟨$⟩ id)             ≈⟨ iso.isoʳ _ CE.refl ⟩
           id                                                      ∎
         }
diff --git a/src/Function/Construct/Setoid.agda b/src/Function/Construct/Setoid.agda
new file mode 100644
index 000000000..3d098a5a9
--- /dev/null
+++ b/src/Function/Construct/Setoid.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --without-K --safe #-}
+
+-- was not ported from old function hierarchy
+
+module Function.Construct.Setoid where
+
+  open import Function.Bundles using (Func; _⟨$⟩_)
+  import Function.Construct.Composition as Comp
+  open import Level using (Level)
+  open import Relation.Binary.Bundles using (Setoid)
+
+
+  private
+    variable
+      a₁ a₂ b₁ b₂ c₁ c₂ : Level
+      
+  function : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
+  function From To = record
+    { Carrier = Func From To
+    ; _≈_ = λ f g → ∀ {x y} → x From.≈ y → f ⟨$⟩ x To.≈ g ⟨$⟩ y
+    ; isEquivalence = record
+      { refl = λ {f} x≈y → Func.cong f x≈y
+      ; sym = λ {f} {g} fx≈gy x≈y → To.sym (fx≈gy (From.sym x≈y))
+      ; trans = λ {f} {g} {h} fx≈gy gx≈hy x≈y → To.trans (fx≈gy x≈y) (gx≈hy From.refl)
+      }
+    }
+    where
+      module To = Setoid To
+      module From = Setoid From
+
+  -- This doesn't really belong here, it should be in Function.Construct.Composition but that's in stdlib
+  -- so will need to be contributed to there first.
+  infixr 9 _∙_
+  _∙_ : {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} {C : Setoid c₁ c₂} → Func B C → Func A B → Func A C
+  f ∙ g = Comp.function g f
+    
+