proposition: Lemma δ_comp_law1 : δ_law1 (functor_compose G1 G2) δ_comp.
proof: Proof. apply nat_trans_eq_alt; intro c; simpl; rewrite !id_left, id_right. etrans. { apply maponpaths, (nat_trans_eq_pointwise (distributive_law1 G2 DL2) (pr1 G1 c)). } etrans. { apply cancel_postcomposition, maponpaths, (nat_trans_eq_pointwise (distributive_law1 G1 DL1) c). } now rewrite id_right; apply functor_id. 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