diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
index 5d426bb25d..8510ab4650 100644
--- a/src/category-theory.lagda.md
+++ b/src/category-theory.lagda.md
@@ -50,6 +50,7 @@ open import category-theory.embeddings-precategories public
 open import category-theory.endomorphisms-in-categories public
 open import category-theory.endomorphisms-in-precategories public
 open import category-theory.epimorphisms-in-large-precategories public
+open import category-theory.equivalence-from-fully-faithful-and-split-essentially-surjective-functor public
 open import category-theory.equivalences-of-categories public
 open import category-theory.equivalences-of-large-precategories public
 open import category-theory.equivalences-of-precategories public
@@ -70,6 +71,7 @@ open import category-theory.fully-faithful-functors-precategories public
 open import category-theory.fully-faithful-maps-precategories public
 open import category-theory.function-categories public
 open import category-theory.function-precategories public
+open import category-theory.functor-curry public
 open import category-theory.functors-categories public
 open import category-theory.functors-from-small-to-large-categories public
 open import category-theory.functors-from-small-to-large-precategories public
diff --git a/src/category-theory/equivalence-from-fully-faithful-and-split-essentially-surjective-functor.lagda.md b/src/category-theory/equivalence-from-fully-faithful-and-split-essentially-surjective-functor.lagda.md
new file mode 100644
index 0000000000..fb3bce4869
--- /dev/null
+++ b/src/category-theory/equivalence-from-fully-faithful-and-split-essentially-surjective-functor.lagda.md
@@ -0,0 +1,262 @@
+# File title
+
+```agda
+module category-theory.equivalence-from-fully-faithful-and-split-essentially-surjective-functor where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.equivalences-of-precategories
+open import category-theory.fully-faithful-functors-precategories
+open import category-theory.functors-precategories
+open import category-theory.isomorphisms-in-precategories
+open import category-theory.maps-precategories
+open import category-theory.natural-isomorphisms-functors-precategories
+open import category-theory.natural-transformations-functors-precategories
+open import category-theory.precategories
+open import category-theory.split-essentially-surjective-functors-precategories
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A functor `F : C → D` that is fully faithful (it induces equivalences
+`φ : C(c₁, c₂) ≃ D(F(c₁), F(c₂))` on homsets) and essentially surjective (for
+every `x : D`, we have some `G(x) : C` and an isomorphism `εₓ : F(G(x)) ≅ x`) is
+an equivalence of categories. The construction proceeds along the following
+lines:
+
+- The inverse functor `G` sends objects `x : D` to `G(x) : C`;
+- Morpisms `f: D(x₁, x₂)` are sent to `φ⁻¹(εₓ₂⁻¹ ∘ f ∘ εₓ₁) : C(G(x₁), G(x₂))`;
+- The unit is given on `c : C` by the preimage along `φ` of `ε` at `F(c)`;
+- The counit is given on `x : D` by `εₓ`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C D : Precategory l1 l2)
+  (F : functor-Precategory C D)
+  (HFF : is-fully-faithful-functor-Precategory C D F)
+  (HES : is-split-essentially-surjective-functor-Precategory C D F)
+  where
+
+  private
+    infixl 10 _∘C_
+
+    _∘C_ : {x y z : obj-Precategory C}
+      → hom-Precategory C y z
+      → hom-Precategory C x y
+      → hom-Precategory C x z
+    _∘C_ f g = comp-hom-Precategory C f g
+
+    infixl 10 _∘D_
+    _∘D_ : {x y z : obj-Precategory D}
+      → hom-Precategory D y z
+      → hom-Precategory D x y
+      → hom-Precategory D x z
+    _∘D_ f g = comp-hom-Precategory D f g
+
+    F₀ : obj-Precategory C → obj-Precategory D
+    F₀ = obj-functor-Precategory C D F
+
+    F₁ : {x y : obj-Precategory C}
+      → hom-Precategory C x y
+      → hom-Precategory D (F₀ x) (F₀ y)
+    F₁ = hom-functor-Precategory C D F
+
+    F₁⁻¹ : {x y : obj-Precategory C}
+      → hom-Precategory D (F₀ x) (F₀ y)
+      → hom-Precategory C x y
+    F₁⁻¹ = map-inv-hom-is-fully-faithful-functor-Precategory C D F HFF
+
+    G : obj-Precategory D → obj-Precategory C
+    G d = pr1 (HES d)
+
+    ε :
+      (d : obj-Precategory D)
+      → iso-Precategory D (F₀ (G d)) d
+    ε d = pr2 (HES d)
+
+  obj-functor-ff-es-equiv : obj-Precategory D → obj-Precategory C
+  obj-functor-ff-es-equiv = G
+
+  hom-functor-ff-es-equiv :
+    {x y : obj-Precategory D}
+    → hom-Precategory D x y
+    → hom-Precategory C (obj-functor-ff-es-equiv x) (obj-functor-ff-es-equiv y)
+  hom-functor-ff-es-equiv {x} {y} f =
+    F₁⁻¹ (hom-inv-iso-Precategory D (ε y) ∘D f ∘D hom-iso-Precategory D (ε x))
+
+  map-functor-ff-es-equiv : map-Precategory D C
+  pr1 map-functor-ff-es-equiv = obj-functor-ff-es-equiv
+  pr2 map-functor-ff-es-equiv = hom-functor-ff-es-equiv
+
+  opaque
+    preserves-comp-hom-functor-ff-es-equiv :
+      preserves-comp-hom-map-Precategory D C map-functor-ff-es-equiv
+    preserves-comp-hom-functor-ff-es-equiv {x} {y} {z} g f = inv (
+        fully-faithful-inv-preserves-comp C D F HFF _ _
+        ∙ ap F₁⁻¹ (
+          associative-comp-hom-Precategory D _ _ _
+          ∙ ap (λ a → _ ∘D _ ∘D a)
+              (inv (associative-comp-hom-Precategory D _ _ _))
+          ∙ ap (λ a → _ ∘D _ ∘D (a ∘D _))
+              (inv (associative-comp-hom-Precategory D _ _ _))
+          ∙ ap (λ a → _ ∘D _ ∘D (a ∘D _ ∘D _))
+              (is-section-hom-inv-iso-Precategory D (ε y))
+          ∙ ap (λ a → _ ∘D (a ∘D _))
+              (left-unit-law-comp-hom-Precategory D _)
+          ∙ associative-comp-hom-Precategory D _ g _
+          ∙ ap (λ a → _ ∘D a)
+              (inv (associative-comp-hom-Precategory D _ _ _))
+          ∙ inv (associative-comp-hom-Precategory D _ _ _)
+      ))
+
+    preserves-id-hom-functor-ff-es-equiv :
+      preserves-id-hom-map-Precategory D C map-functor-ff-es-equiv
+    preserves-id-hom-functor-ff-es-equiv x =
+      ap F₁⁻¹ (
+        ap (λ a → a ∘D _) (right-unit-law-comp-hom-Precategory D _)
+        ∙ is-retraction-hom-inv-iso-Precategory D (ε x)
+      ) ∙ inv (fully-faithful-inv-preserves-id C D F HFF _)
+
+  functor-ff-es-equiv : functor-Precategory D C
+  pr1 functor-ff-es-equiv = obj-functor-ff-es-equiv
+  pr1 (pr2 functor-ff-es-equiv) = hom-functor-ff-es-equiv
+  pr1 (pr2 (pr2 functor-ff-es-equiv)) = preserves-comp-hom-functor-ff-es-equiv
+  pr2 (pr2 (pr2 functor-ff-es-equiv)) = preserves-id-hom-functor-ff-es-equiv
+
+  module _
+    (x : obj-Precategory C)
+    where
+
+    iso-unit-ff-es-equiv :
+      iso-Precategory C
+        (obj-functor-Precategory C C
+          (comp-functor-Precategory C D C functor-ff-es-equiv F) x)
+        x
+    iso-unit-ff-es-equiv =
+      (is-essentially-injective-is-fully-faithful-functor-Precategory
+        C D F HFF _ _ (ε (F₀ x)))
+
+    hom-unit-ff-es-equiv :
+      hom-Precategory C
+        (obj-functor-Precategory C C
+          (comp-functor-Precategory C D C functor-ff-es-equiv F) x)
+        x
+    hom-unit-ff-es-equiv = hom-iso-Precategory C iso-unit-ff-es-equiv
+
+    is-iso-unit-ff-es-equiv : is-iso-Precategory C hom-unit-ff-es-equiv
+    is-iso-unit-ff-es-equiv = is-iso-iso-Precategory C iso-unit-ff-es-equiv
+
+  opaque
+    is-natural-unit-ff-es-equiv :
+      is-natural-transformation-Precategory C C
+        (comp-functor-Precategory C D C functor-ff-es-equiv F)
+        (id-functor-Precategory C)
+        hom-unit-ff-es-equiv
+    is-natural-unit-ff-es-equiv {x} {y} f = equational-reasoning
+        f ∘C hom-unit-ff-es-equiv x
+      ＝ F₁⁻¹ (F₁ f) ∘C hom-unit-ff-es-equiv x
+        by ap (λ a → a ∘C _)
+          (inv (is-retraction-map-section-is-equiv (HFF _ _) f))
+      ＝ F₁⁻¹ (F₁ f ∘D (hom-iso-Precategory D (ε (F₀ x))))
+        by fully-faithful-inv-preserves-comp C D F HFF _ _
+      ＝ F₁⁻¹ (
+          (id-hom-Precategory D)
+          ∘D (F₁ f)
+          ∘D (hom-iso-Precategory D (ε (F₀ x))))
+        by ap (λ a → F₁⁻¹ (a ∘D _))
+          (inv (left-unit-law-comp-hom-Precategory D _))
+      ＝ F₁⁻¹ (
+          (hom-iso-Precategory D (ε (F₀ y)))
+          ∘D (hom-inv-iso-Precategory D (ε (F₀ y)))
+          ∘D (F₁ f)
+          ∘D (hom-iso-Precategory D (ε (F₀ x))))
+        by ap (λ a → F₁⁻¹ (a ∘D _ ∘D _))
+          (inv (is-section-hom-inv-iso-Precategory D (ε (F₀ y))))
+      ＝ F₁⁻¹ (
+          (hom-iso-Precategory D (ε (F₀ y)))
+          ∘D (
+            (hom-inv-iso-Precategory D (ε (F₀ y)))
+            ∘D (F₁ f)
+            ∘D (hom-iso-Precategory D (ε (F₀ x)))))
+        by ap F₁⁻¹ (
+          associative-comp-hom-Precategory D _ _ _
+          ∙ associative-comp-hom-Precategory D _ _ _
+          ∙ ap (λ a → _ ∘D a) (inv (associative-comp-hom-Precategory D _ _ _)))
+      ＝ (hom-unit-ff-es-equiv y) ∘C (hom-functor-ff-es-equiv (F₁ f))
+        by inv (fully-faithful-inv-preserves-comp C D F HFF _ _)
+
+  unit-ff-es-equiv :
+    natural-isomorphism-Precategory C C
+      (comp-functor-Precategory C D C functor-ff-es-equiv F)
+      (id-functor-Precategory C)
+  pr1 (pr1 unit-ff-es-equiv) = hom-unit-ff-es-equiv
+  pr2 (pr1 unit-ff-es-equiv) = is-natural-unit-ff-es-equiv
+  pr2 unit-ff-es-equiv = is-iso-unit-ff-es-equiv
+
+  hom-counit-ff-es-equiv :
+    (d : obj-Precategory D)
+    → hom-Precategory D
+      (obj-functor-Precategory D D
+        (comp-functor-Precategory D C D F functor-ff-es-equiv) d) d
+  hom-counit-ff-es-equiv d = hom-iso-Precategory D (ε d)
+
+  is-iso-counit-ff-es-equiv :
+    (d : obj-Precategory D)
+    → is-iso-Precategory D (hom-counit-ff-es-equiv d)
+  is-iso-counit-ff-es-equiv d = is-iso-iso-Precategory D (ε d)
+
+  opaque
+    is-natural-counit-ff-es-equiv :
+      is-natural-transformation-Precategory D D
+        (comp-functor-Precategory D C D F functor-ff-es-equiv)
+        (id-functor-Precategory D)
+        hom-counit-ff-es-equiv
+    is-natural-counit-ff-es-equiv {x} {y} f = equational-reasoning
+      f ∘D (hom-counit-ff-es-equiv x)
+      ＝ (id-hom-Precategory D) ∘D f ∘D (hom-counit-ff-es-equiv x)
+        by ap (λ a → a ∘D _) (inv (left-unit-law-comp-hom-Precategory D f))
+      ＝ (hom-iso-Precategory D (ε y))
+          ∘D (hom-inv-iso-Precategory D (ε y))
+          ∘D f
+          ∘D (hom-counit-ff-es-equiv x)
+        by ap (λ a → a ∘D _ ∘D _)
+          (inv (is-section-hom-inv-iso-Precategory D (ε y)))
+      ＝ (hom-iso-Precategory D (ε y))
+          ∘D (
+            (hom-inv-iso-Precategory D (ε y))
+            ∘D f
+            ∘D (hom-iso-Precategory D (ε x)))
+        by associative-comp-hom-Precategory D _ _ _
+          ∙ associative-comp-hom-Precategory D _ _ _
+          ∙ ap (λ a → _ ∘D a) (inv (associative-comp-hom-Precategory D _ _ _))
+      ＝ (hom-counit-ff-es-equiv y) ∘D (F₁ (hom-functor-ff-es-equiv f))
+        by ap (λ a → _ ∘D a) (inv (is-section-map-section-is-equiv (HFF _ _) _))
+
+  counit-ff-es-equiv :
+    natural-isomorphism-Precategory D D
+      (comp-functor-Precategory D C D F functor-ff-es-equiv)
+      (id-functor-Precategory D)
+  pr1 (pr1 counit-ff-es-equiv) = hom-counit-ff-es-equiv
+  pr2 (pr1 counit-ff-es-equiv) = is-natural-counit-ff-es-equiv
+  pr2 counit-ff-es-equiv = is-iso-counit-ff-es-equiv
+
+  result : equiv-Precategory C D
+  pr1 result = F
+  pr1 (pr1 (pr2 result)) = functor-ff-es-equiv
+  pr2 (pr1 (pr2 result)) = unit-ff-es-equiv
+  pr1 (pr2 (pr2 result)) = functor-ff-es-equiv
+  pr2 (pr2 (pr2 result)) = counit-ff-es-equiv
+```
diff --git a/src/category-theory/fully-faithful-functors-precategories.lagda.md b/src/category-theory/fully-faithful-functors-precategories.lagda.md
index a0de4952c0..ddd26515c5 100644
--- a/src/category-theory/fully-faithful-functors-precategories.lagda.md
+++ b/src/category-theory/fully-faithful-functors-precategories.lagda.md
@@ -409,6 +409,65 @@ module _
       { x} {y}
 ```
 
+### The inverse function on the morphisms preserves composition and identity
+
+```agda
+module _
+  {l1 l2 : Level}
+  (C D : Precategory l1 l2)
+  (F : functor-Precategory C D)
+  (H : is-fully-faithful-functor-Precategory C D F)
+  where
+
+  module _
+    {x y z : obj-Precategory C}
+    (f : hom-Precategory D (obj-functor-Precategory C D F y)
+      (obj-functor-Precategory C D F z))
+    (g : hom-Precategory D (obj-functor-Precategory C D F x)
+      (obj-functor-Precategory C D F y))
+    where
+
+    private
+      f' : hom-Precategory C y z
+      f' = map-inv-hom-is-fully-faithful-functor-Precategory C D F H f
+
+      g' : hom-Precategory C x y
+      g' = map-inv-hom-is-fully-faithful-functor-Precategory C D F H g
+
+    fully-faithful-inv-preserves-comp :
+      comp-hom-Precategory C f' g'
+      ＝ map-inv-hom-is-fully-faithful-functor-Precategory C D F H
+        (comp-hom-Precategory D f g)
+    fully-faithful-inv-preserves-comp
+      = inv (is-retraction-map-section-is-equiv (H x z)
+        (comp-hom-Precategory C f' g'))
+      ∙ ap (λ a → map-inv-hom-is-fully-faithful-functor-Precategory C D F H a) (
+        preserves-comp-functor-Precategory C D F f' g'
+        ∙ ap (λ a → comp-hom-Precategory D a _)
+          (is-section-map-section-is-equiv (H y z) f)
+        ∙ ap (λ a → comp-hom-Precategory D _ a)
+          (is-section-map-section-is-equiv (H x y) g)
+      )
+
+  module _
+    (x : obj-Precategory C)
+    where
+
+    private
+      x' : obj-Precategory D
+      x' = obj-functor-Precategory C D F x
+
+    fully-faithful-inv-preserves-id :
+      id-hom-Precategory C {x}
+      ＝ map-inv-hom-is-fully-faithful-functor-Precategory C D F H
+        (id-hom-Precategory D {x'})
+
+    fully-faithful-inv-preserves-id
+      = inv (is-retraction-map-section-is-equiv (H x x) (id-hom-Precategory C))
+        ∙ ap (λ a → map-inv-hom-is-fully-faithful-functor-Precategory C D F H a)
+          (preserves-id-functor-Precategory C D F x)
+```
+
 ## External links
 
 - [Fully Faithful Functors](https://1lab.dev/Cat.Functor.Properties.html#fully-faithful-functors)
diff --git a/src/category-theory/functor-curry.lagda.md b/src/category-theory/functor-curry.lagda.md
new file mode 100644
index 0000000000..63bfdf76dc
--- /dev/null
+++ b/src/category-theory/functor-curry.lagda.md
@@ -0,0 +1,319 @@
+# The Currying of Functors on a Product Category
+
+```agda
+module category-theory.functor-curry where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.functors-precategories
+open import category-theory.maps-precategories
+open import category-theory.natural-transformations-functors-precategories
+open import category-theory.precategories
+open import category-theory.precategory-of-functors
+open import category-theory.products-of-precategories
+
+open import foundation.action-on-identifications-functions
+open import foundation.equality-cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+In the context of sets, currying means that we can view a function
+`f : S × T → U` as a function `f : S → (T → U)`. We can view this as a function
+`curry : (S × T → U) → (S → T → U)`. In the context of categories, there is a
+similar situation: this file constructs the functor between functor categories
+
+```text
+curry-functor : [C × D, E] → [C, [D, E]].
+```
+
+## Definition
+
+```agda
+module CurryFunctor
+  {lc₁ lc₂ ld₁ ld₂ le₁ le₂ : Level}
+  (C : Precategory lc₁ lc₂)
+  (D : Precategory ld₁ ld₂)
+  (E : Precategory le₁ le₂) where
+  private
+    CD = product-Precategory C D
+    CDE1 = functor-precategory-Precategory CD E
+    DE = functor-precategory-Precategory D E
+    CDE2 = functor-precategory-Precategory C DE
+
+  module _
+    (F : obj-Precategory CDE1)
+    where
+
+    module _
+      (c : obj-Precategory C)
+      where
+
+      obj-obj-obj-curry-functor : obj-Precategory D → obj-Precategory E
+      obj-obj-obj-curry-functor d = obj-functor-Precategory CD E F (c , d)
+
+      hom-obj-obj-curry-functor :
+        {d₁ d₂ : obj-Precategory D}
+        → hom-Precategory D d₁ d₂
+        → hom-Precategory E
+          (obj-obj-obj-curry-functor d₁)
+          (obj-obj-obj-curry-functor d₂)
+      hom-obj-obj-curry-functor f =
+        hom-functor-Precategory CD E F (id-hom-Precategory C , f)
+
+      map-obj-obj-curry-functor : map-Precategory D E
+      pr1 map-obj-obj-curry-functor = obj-obj-obj-curry-functor
+      pr2 map-obj-obj-curry-functor = hom-obj-obj-curry-functor
+
+      opaque
+        preserves-comp-obj-obj-curry-functor :
+          preserves-comp-hom-map-Precategory D E map-obj-obj-curry-functor
+        preserves-comp-obj-obj-curry-functor f g = equational-reasoning
+          hom-functor-Precategory CD E F
+            (id-hom-Precategory C , comp-hom-Precategory D f g)
+          ＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
+              (id-hom-Precategory C , f) (id-hom-Precategory C , g))
+            by ap (λ x → hom-functor-Precategory CD E F (x , _)) (inv
+              (left-unit-law-comp-hom-Precategory C (id-hom-Precategory C)))
+          ＝ comp-hom-Precategory E
+              (hom-functor-Precategory CD E F (id-hom-Precategory C , f))
+              (hom-functor-Precategory CD E F (id-hom-Precategory C , g))
+            by preserves-comp-functor-Precategory CD E F
+              (id-hom-Precategory C , f)
+              (id-hom-Precategory C , g)
+
+        preserves-id-obj-obj-curry-functor :
+          preserves-id-hom-map-Precategory D E map-obj-obj-curry-functor
+        preserves-id-obj-obj-curry-functor d =
+          preserves-id-functor-Precategory CD E F (c , d)
+
+      obj-obj-curry-functor : obj-Precategory DE
+      pr1 obj-obj-curry-functor = obj-obj-obj-curry-functor
+      pr1 (pr2 obj-obj-curry-functor) = hom-obj-obj-curry-functor
+      pr1 (pr2 (pr2 obj-obj-curry-functor)) =
+        preserves-comp-obj-obj-curry-functor
+      pr2 (pr2 (pr2 obj-obj-curry-functor)) = preserves-id-obj-obj-curry-functor
+
+    module _
+      {c₁ c₂ : obj-Precategory C}
+      (f : hom-Precategory C c₁ c₂)
+      where
+
+      hom-hom-obj-curry-functor :
+        (d : obj-Precategory D)
+        → hom-Precategory E
+          (obj-obj-obj-curry-functor c₁ d)
+          (obj-obj-obj-curry-functor c₂ d)
+      hom-hom-obj-curry-functor d =
+        hom-functor-Precategory CD E F (f , id-hom-Precategory D)
+
+      opaque
+        is-natural-hom-obj-curry-functor :
+          is-natural-transformation-Precategory D E
+            (obj-obj-curry-functor c₁) (obj-obj-curry-functor c₂)
+            hom-hom-obj-curry-functor
+        is-natural-hom-obj-curry-functor {d₁} {d₂} g = equational-reasoning
+          comp-hom-Precategory E
+            (hom-obj-obj-curry-functor c₂ g)
+            (hom-hom-obj-curry-functor d₁)
+          ＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
+              (id-hom-Precategory C , g)
+              (f , id-hom-Precategory D))
+            by inv (preserves-comp-functor-Precategory CD E F
+              (id-hom-Precategory C , g)
+              (f , id-hom-Precategory D))
+          ＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
+              (f , id-hom-Precategory D)
+              (id-hom-Precategory C , g))
+            by ap (hom-functor-Precategory CD E F) (eq-pair
+              (left-unit-law-comp-hom-Precategory C f
+                ∙ inv (right-unit-law-comp-hom-Precategory C f))
+              (right-unit-law-comp-hom-Precategory D g
+                ∙ inv (left-unit-law-comp-hom-Precategory D g)))
+          ＝ comp-hom-Precategory E
+              (hom-hom-obj-curry-functor d₂)
+              (hom-obj-obj-curry-functor c₁ g)
+            by preserves-comp-functor-Precategory CD E F
+              (f , id-hom-Precategory D)
+              (id-hom-Precategory C , g)
+
+      hom-obj-curry-functor :
+        hom-Precategory DE (obj-obj-curry-functor c₁) (obj-obj-curry-functor c₂)
+      pr1 hom-obj-curry-functor = hom-hom-obj-curry-functor
+      pr2 hom-obj-curry-functor = is-natural-hom-obj-curry-functor
+
+    map-obj-curry-functor : map-Precategory C DE
+    pr1 map-obj-curry-functor = obj-obj-curry-functor
+    pr2 map-obj-curry-functor = hom-obj-curry-functor
+
+    opaque
+      preserves-comp-obj-curry-functor :
+        preserves-comp-hom-map-Precategory C DE map-obj-curry-functor
+      preserves-comp-obj-curry-functor {c₁} {c₂} {c₃} f g =
+        eq-htpy-hom-family-natural-transformation-Precategory
+        D E
+        (obj-obj-curry-functor c₁) (obj-obj-curry-functor c₃)
+        (hom-obj-curry-functor (comp-hom-Precategory C f g))
+        (comp-hom-Precategory DE
+          {obj-obj-curry-functor c₁}
+          {obj-obj-curry-functor c₂}
+          {obj-obj-curry-functor c₃}
+          (hom-obj-curry-functor f)
+          (hom-obj-curry-functor g))
+        (λ d → equational-reasoning
+          hom-functor-Precategory CD E F
+            (comp-hom-Precategory C f g , id-hom-Precategory D)
+          ＝ hom-functor-Precategory CD E F (comp-hom-Precategory CD
+              (f , id-hom-Precategory D)
+              (g , id-hom-Precategory D))
+            by ap
+              (λ h → hom-functor-Precategory CD E F
+                (comp-hom-Precategory C f g , h))
+              (inv
+                (left-unit-law-comp-hom-Precategory D (id-hom-Precategory D)))
+          ＝ comp-hom-Precategory E
+              (hom-functor-Precategory CD E F (f , id-hom-Precategory D))
+              (hom-functor-Precategory CD E F (g , id-hom-Precategory D))
+          by preserves-comp-functor-Precategory CD E F
+            (f , id-hom-Precategory D)
+            (g , id-hom-Precategory D))
+
+      preserves-id-obj-curry-functor :
+        preserves-id-hom-map-Precategory C DE map-obj-curry-functor
+      preserves-id-obj-curry-functor c =
+        eq-htpy-hom-family-natural-transformation-Precategory
+        D E
+        (obj-obj-curry-functor c)
+        (obj-obj-curry-functor c)
+        (hom-obj-curry-functor (id-hom-Precategory C))
+        (id-hom-Precategory DE {obj-obj-curry-functor c})
+        (λ d → preserves-id-functor-Precategory CD E F (c , d))
+
+    obj-curry-functor : obj-Precategory CDE2
+    pr1 obj-curry-functor = obj-obj-curry-functor
+    pr1 (pr2 obj-curry-functor) = hom-obj-curry-functor
+    pr1 (pr2 (pr2 obj-curry-functor)) = preserves-comp-obj-curry-functor
+    pr2 (pr2 (pr2 obj-curry-functor)) = preserves-id-obj-curry-functor
+
+  module _
+    {F₁ F₂ : obj-Precategory CDE1}
+    (α : hom-Precategory CDE1 F₁ F₂)
+    where
+
+    module _
+      (c : obj-Precategory C)
+      where
+
+      hom-hom-hom-curry-functor :
+        (d : obj-Precategory D)
+        → hom-Precategory E
+          (obj-obj-obj-curry-functor F₁ c d)
+          (obj-obj-obj-curry-functor F₂ c d)
+      hom-hom-hom-curry-functor d =
+        hom-family-natural-transformation-Precategory CD E F₁ F₂ α (c , d)
+
+      opaque
+        is-natural-hom-hom-curry-functor :
+          is-natural-transformation-Precategory D E
+            (obj-obj-curry-functor F₁ c) (obj-obj-curry-functor F₂ c)
+            hom-hom-hom-curry-functor
+        is-natural-hom-hom-curry-functor {d₁} {d₂} f =
+          naturality-natural-transformation-Precategory CD E F₁ F₂ α
+          (id-hom-Precategory C , f)
+
+      hom-hom-curry-functor :
+        hom-Precategory DE
+          (obj-obj-curry-functor F₁ c) (obj-obj-curry-functor F₂ c)
+      pr1 hom-hom-curry-functor = hom-hom-hom-curry-functor
+      pr2 hom-hom-curry-functor = is-natural-hom-hom-curry-functor
+
+    opaque
+      is-natural-hom-curry-functor :
+        is-natural-transformation-Precategory C DE
+          (obj-curry-functor F₁) (obj-curry-functor F₂)
+          hom-hom-curry-functor
+      is-natural-hom-curry-functor {c₁} {c₂} f =
+        eq-htpy-hom-family-natural-transformation-Precategory
+        D E
+        (obj-obj-curry-functor F₁ c₁) (obj-obj-curry-functor F₂ c₂)
+        (comp-hom-Precategory DE
+          {obj-obj-curry-functor F₁ c₁}
+          {obj-obj-curry-functor F₂ c₁}
+          {obj-obj-curry-functor F₂ c₂}
+          (hom-obj-curry-functor F₂ f)
+          (hom-hom-curry-functor c₁))
+        (comp-hom-Precategory DE
+          {obj-obj-curry-functor F₁ c₁}
+          {obj-obj-curry-functor F₁ c₂}
+          {obj-obj-curry-functor F₂ c₂}
+          (hom-hom-curry-functor c₂)
+          (hom-obj-curry-functor F₁ f))
+        (λ d → naturality-natural-transformation-Precategory CD E F₁ F₂ α
+          (f , id-hom-Precategory D))
+
+    hom-curry-functor :
+      hom-Precategory CDE2 (obj-curry-functor F₁) (obj-curry-functor F₂)
+    pr1 hom-curry-functor = hom-hom-curry-functor
+    pr2 hom-curry-functor = is-natural-hom-curry-functor
+
+  map-curry-functor : map-Precategory CDE1 CDE2
+  pr1 map-curry-functor = obj-curry-functor
+  pr2 map-curry-functor {F₁} {F₂} = hom-curry-functor {F₁} {F₂}
+
+  opaque
+    preserves-comp-curry-functor :
+      preserves-comp-hom-map-Precategory CDE1 CDE2 map-curry-functor
+    preserves-comp-curry-functor {F₁} {F₂} {F₃} α₁ α₂ =
+      eq-htpy-hom-family-natural-transformation-Precategory
+      C DE
+      (obj-curry-functor F₁) (obj-curry-functor F₃)
+      (hom-curry-functor {F₁} {F₃}
+        (comp-hom-Precategory CDE1 {F₁} {F₂} {F₃} α₁ α₂))
+      (comp-hom-Precategory CDE2
+        {obj-curry-functor F₁}
+        {obj-curry-functor F₂}
+        {obj-curry-functor F₃}
+        (hom-curry-functor {F₂} {F₃} α₁)
+        (hom-curry-functor {F₁} {F₂} α₂))
+      (λ c → eq-htpy-hom-family-natural-transformation-Precategory
+        D E
+        (obj-obj-curry-functor F₁ c) (obj-obj-curry-functor F₃ c)
+        (hom-hom-curry-functor {F₁} {F₃}
+          (comp-hom-Precategory CDE1 {F₁} {F₂} {F₃} α₁ α₂) c)
+        (comp-hom-Precategory DE
+          {obj-obj-curry-functor F₁ c}
+          {obj-obj-curry-functor F₂ c}
+          {obj-obj-curry-functor F₃ c}
+          (hom-hom-curry-functor {F₂} {F₃} α₁ c)
+          (hom-hom-curry-functor {F₁} {F₂} α₂ c))
+        (λ d → refl))
+
+    preserves-id-curry-functor :
+      preserves-id-hom-map-Precategory CDE1 CDE2 map-curry-functor
+    preserves-id-curry-functor F =
+      eq-htpy-hom-family-natural-transformation-Precategory
+      C DE
+      (obj-curry-functor F) (obj-curry-functor F)
+      (hom-curry-functor {F} {F} (id-hom-Precategory CDE1 {F}))
+      (id-hom-Precategory CDE2 {obj-curry-functor F})
+      (λ c → eq-htpy-hom-family-natural-transformation-Precategory
+        D E
+        (obj-obj-curry-functor F c) (obj-obj-curry-functor F c)
+        (hom-hom-curry-functor {F} {F} (id-hom-Precategory CDE1 {F}) c)
+        (id-hom-Precategory DE {obj-obj-curry-functor F c})
+        (λ d → refl))
+
+  curry-functor : functor-Precategory CDE1 CDE2
+  pr1 curry-functor = obj-curry-functor
+  pr1 (pr2 curry-functor) {F₁} {F₂} = hom-curry-functor {F₁} {F₂}
+  pr1 (pr2 (pr2 curry-functor)) {F₁} {F₂} {F₃} =
+    preserves-comp-curry-functor {F₁} {F₂} {F₃}
+  pr2 (pr2 (pr2 curry-functor)) = preserves-id-curry-functor
+```