Lemma comp_distr_laws_assoc {C C' C'' C''' D D' D'' D''' : category} {F : functor C D} {F' : functor C' D'} {F'' : functor C'' D''} {F''' : functor C''' D'''} {H : functor C' C} {H' : functor C'' C'} {H'' : functor C''' C''} {K : functor D' D} {K' : functor D'' D'} {K'' : functor D''' D''} (lambda : DistrLaw F F' H K) (lambda' : DistrLaw F' F'' H' K') (lambda'' : DistrLaw F'' F''' H'' K'') : comp_distr_laws (comp_distr_laws lambda lambda') lambda'' = comp_distr_laws lambda (comp_distr_laws lambda' lambda''). Proof. apply nat_trans_eq_alt. intro c. simpl. repeat rewrite id_left. repeat rewrite id_right. set (aux1 := nat_trans_ax lambda). eapply pathscomp0. { apply pathsinv0. apply assoc. } apply cancel_precomposition. apply pathsinv0. etrans. { apply functor_comp. } apply cancel_precomposition. apply idpath. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Adjunctions.Core.