proposition: Lemma lax_lineator_binprod_indirect_data_ok (v : V) (c : C): lax_lineator_binprod_indirect v c = binprod_collector_data Mon_V BPD ActD v (F1 c) (F2 c) · BinProductOfArrows _ (BPD _ _) (BPD _ _) (ll1 v c) (ll2 v c).
proof: Proof. unfold lax_lineator_binprod_indirect. Abort. Definition lineator_data_binprod: lineator_data Mon_V ActC ActD FF. Proof. intros v c. exact (binprod_collector_data Mon_V BPD ActD v (F1 c) (F2 c) · BinProductOfArrows _ (BPD _ _) (BPD _ _) (ll1 v c) (ll2 v c)). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories UniMath.CategoryTheory.Actegories.ConstructionOfActegories UniMath.CategoryTheory.coslicecat UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Actegories.CoproductsInActegories UniMath.CategoryTheory.Actegories.ProductsInActegories UniMath.CategoryTheory.Actegories.ProductActegory