Definition uncurry_nattrans : uncurry_functor F ⟹ uncurry_functor G. Proof. use make_nat_trans. - intro cd. cbn. exact (pr1 (α (pr2 cd)) (pr1 cd)). - intros cd cd' fg. induction cd as [c d]. induction cd' as [c' d']. induction fg as [f g]. cbn in *. assert (aux := nat_trans_ax α d d' g). apply (maponpaths pr1) in aux. apply toforallpaths in aux. assert (auxinst := aux c'). rewrite <- assoc. etrans. { apply maponpaths. exact auxinst. } clear aux auxinst. cbn. do 2 rewrite assoc. apply cancel_postcomposition. apply nat_trans_ax. 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.