proposition: Proposition structure_copows_mor_in (X : category_of_hset_struct P) (x : C) : mor_hset_struct P (pr2 X) (E x (structure_copows_coprod X x)) structure_copows_in.
proof: Proof. exact (pr1 (pr2 HE X x)). 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