proposition: Lemma δ_comp_law2 : δ_law2 (functor_compose G1 G2) δ_comp.
proof: Proof. intros Ze Ze'. apply nat_trans_eq_alt; intro c; simpl; rewrite !id_left, !id_right. etrans. { apply cancel_postcomposition, maponpaths, (nat_trans_eq_pointwise (distributive_law2 G1 DL1 Ze Ze') c). } etrans. { apply maponpaths, (nat_trans_eq_pointwise (distributive_law2 G2 DL2 Ze Ze') (pr1 G1 c)). } simpl; rewrite !id_left, !id_right. etrans. { apply cancel_postcomposition, functor_comp. } rewrite <- !assoc. apply maponpaths. rewrite assoc. etrans. { apply cancel_postcomposition, (nat_trans_ax (δ G2 DL2 Ze') _ _ (pr1 (δ G1 DL1 Ze) c)). } simpl; rewrite <- !assoc. now apply maponpaths, pathsinv0, functor_comp. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.PointedFunctors UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.BicatOfCatsElementary UniMath.SubstitutionSystems.Notation UniMath.CategoryTheory.PointedFunctorsComposition