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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coproducts. Import MonoidalNotations. Section CoproductFromUnderlying. End CoproductFromUnderlying.