proposition: Proposition structure_enrichment_obj_coprod_sum_in {x : C} {ys : J → C} (fs : ∏ (j : J), ys j --> x) (j : J) : structure_enrichment_obj_coprod_in ys j · structure_enrichment_obj_coprod_sum fs = fs j.
proof: Proof. apply CoproductInCommutes. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.Examples.StructureEnriched UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedInitial UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedBinaryCoproducts UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoproducts UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Monoidal.Examples.StructuresMonoidal UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Coequalizers