proposition: Proposition isaprop_enrichment_coprod {V : monoidal_cat} {C : category} (HC : is_univalent C) (E : enrichment C V) (J : UU) : isaprop (enrichment_coprod E J).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use funextsec ; intro D. use subtypePath. { intro. apply isaprop_is_coprod_enriched. } use total2_paths_f. - use (isotoid _ HC). use iso_between_coproduct_enriched. + exact (pr2 (φ₁ D)). + exact (pr2 (φ₂ D)). - rewrite transportf_sec_constant. use funextsec. intro j. rewrite transportf_enriched_arr_r. rewrite idtoiso_isotoid. cbn. refine (_ @ enriched_from_to_arr E _). apply maponpaths. unfold map_between_coproduct_enriched ; cbn. etrans. { apply is_coprod_enriched_arrow_in. } apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coproducts