proposition: Lemma is_nat_trans_comp {C : precategory_data}{C' : precategory} {F G H : functor_data C C'} (a : nat_trans F G) (b : nat_trans G H): is_nat_trans F H (λ x : ob C, a x · b x).
proof: Proof. intros ? ? ?. now rewrite assoc, nat_trans_ax, <- assoc, nat_trans_ax, assoc. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence