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. intros ? ? ?. now rewrite assoc, nat_trans_ax, <- assoc, nat_trans_ax, assoc. 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.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence.