Definition curry_functor'_mor {x₁ x₂ : D₁} (f : x₁ --> x₂) : curry_functor'_point x₁ ⟹ curry_functor'_point x₂. Proof. use make_nat_trans. - refine (λ y, #F (_ ,, _)). + exact f. + exact (identity y). - abstract (intros y₁ y₂ g ; cbn ; rewrite <- !(functor_comp F) ; cbn ; rewrite !id_left, !id_right ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat.