proposition: Lemma nat_trans_from_functor_fix_snd_morphism_arg_ax: is_nat_trans _ _ nat_trans_from_functor_fix_snd_morphism_arg_data.
proof: Proof. red. intros c c' g. unfold nat_trans_from_functor_fix_snd_morphism_arg_data. unfold functor_fix_snd_arg; cbn. unfold functor_fix_snd_arg_mor; simpl. eapply pathscomp0. 2: { apply functor_comp. } apply pathsinv0. eapply pathscomp0. 2: { apply functor_comp. } apply maponpaths. unfold compose. cbn. do 2 rewrite id_left. do 2 rewrite id_right. apply idpath. 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