proposition: Lemma uncurry_functor_data_is_functor: is_functor uncurry_functor_data.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat