Lemma uncurry_functor_data_is_functor: is_functor uncurry_functor_data. Proof. split. - intro cd. induction cd as [c d]. cbn. rewrite functor_id. rewrite id_left. assert (H := functor_id G d). apply (maponpaths (fun f => pr1 f c)) in H. exact H. - intros cd1 cd2 cd3 ff' gg'. induction cd1 as [c1 d1]. induction cd2 as [c2 d2]. induction cd3 as [c3 d3]. induction ff' as [f f']. induction gg' as [g g']. cbn in *. rewrite functor_comp. assert (H := functor_comp G f' g'). apply (maponpaths (fun f => pr1 f c3)) in H. etrans. { apply maponpaths. exact H. } cbn. repeat rewrite assoc. apply cancel_postcomposition. repeat rewrite <- assoc. apply maponpaths. apply nat_trans_ax. Qed.
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.