Definition comp_distr_laws {C C' C'' D D' D'' : category}{F : functor C D}{F' : functor C' D'} {F'' : functor C'' D''}{H : functor C' C}{H' : functor C'' C'}{K : functor D' D}{K' : functor D'' D'} (lambda : DistrLaw F F' H K) (lambda' : DistrLaw F' F'' H' K') : DistrLaw F F'' (H' ∙ H ) (K' ∙ K). Proof. red. apply (nat_trans_comp _ _ _ (α_functors _ _ _)). use (nat_trans_comp _ _ _ _ (α_functors _ _ _)). apply (nat_trans_comp _ _ _ (pre_whisker H' lambda)). apply (nat_trans_comp _ _ _ (α_functors_inv _ _ _)). exact (post_whisker lambda' K). Defined.
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.