proposition: Lemma δ_law2_genoption : δ_law2 genopt δ_genoption.
proof: Proof. intros Ze Z'e'; induction Ze as [Z e]; induction Z'e' as [Z' e']. apply nat_trans_eq_alt; intro c; simpl. unfold δ_genoption_mor, BinCoproduct_of_functors_ob; simpl. rewrite !id_left, id_right. apply pathsinv0, BinCoproductArrowUnique. - rewrite assoc. etrans. { apply cancel_postcomposition, BinCoproductIn1Commutes. } rewrite <- assoc. etrans. { apply maponpaths, pathsinv0, (nat_trans_ax e'). } simpl; rewrite assoc. etrans. { apply cancel_postcomposition, BinCoproductIn1Commutes. } rewrite <- !assoc. now apply maponpaths. - rewrite assoc. etrans. { apply cancel_postcomposition, BinCoproductIn2Commutes. } etrans. { apply pathsinv0, functor_comp. } now apply maponpaths, BinCoproductIn2Commutes. 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