proposition: Lemma cop_ff_comul_ax : is_nat_trans _ _ cop_ff_comul_data.
proof: Proof. intros f g γ. use arrow_mor_eq. - etrans. apply id_right. apply pathsinv0. apply id_left. - use BinCoproductArrowsEq. * etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn1Commutes. etrans. apply assoc'. etrans. apply cancel_precomposition. apply BinCoproductIn1Commutes. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn1Commutes. etrans. apply BinCoproductIn1Commutes. reflexivity. * etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn2Commutes. etrans. apply assoc'. etrans. apply cancel_precomposition. apply BinCoproductIn2Commutes. apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn2Commutes. etrans. apply assoc'. etrans. apply cancel_precomposition. apply BinCoproductIn2Commutes. etrans. apply assoc. etrans. apply cancel_postcomposition. apply BinCoproductIn2Commutes. apply assoc'. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LiftingWithClass UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three