proposition: Lemma monads_category_comp_subproof {F F' F'' : functor C C} (T : disp_Monad_data F) (Tlaws : disp_Monad_laws T) (T' : disp_Monad_data F') (T'laws : disp_Monad_laws T') (T'' : disp_Monad_data F'') (T''laws : disp_Monad_laws T'') (α : F ⟹ F') (α' : F' ⟹ F'') : disp_Monad_Mor_laws T T' α → disp_Monad_Mor_laws T' T'' α' → disp_Monad_Mor_laws T T'' (nat_trans_comp _ _ _ α α').
proof: Proof. intros Hα Hα'. split; intros; simpl. - rewrite assoc. set (H:=pr1 Hα a); simpl in H. rewrite H; clear H; rewrite <- !assoc. set (H:=pr1 Hα' a); simpl in H. rewrite H; clear H. rewrite functor_comp. apply maponpaths. now rewrite !assoc, nat_trans_ax. - rewrite assoc. eapply pathscomp0; [apply cancel_postcomposition, (pr2 Hα)|]. apply (pr2 Hα'). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Core.Univalence