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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence.