Lemma nat_trans_from_functor_fix_snd_morphism_arg_ax: is_nat_trans _ _ nat_trans_from_functor_fix_snd_morphism_arg_data. 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.
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.