Proposition isaprop_enrichment_binary_coprod {V : monoidal_cat} {C : category} (HC : is_univalent C) (E : enrichment C V) : isaprop (enrichment_binary_coprod E). Proof. use invproofirrelevance. intros φ₁ φ₂. use funextsec ; intro x. use funextsec ; intro y. use subtypePath. { intro. apply isaprop_is_binary_coprod_enriched. } use total2_paths_f. - use (isotoid _ HC). use iso_between_coproduct_enriched. + exact (pr2 (φ₁ x y)). + exact (pr2 (φ₂ x y)). - rewrite transportf_dirprod. use pathsdirprod. + rewrite transportf_enriched_arr_r. rewrite idtoiso_isotoid. cbn. refine (_ @ enriched_from_to_arr E _). apply maponpaths. unfold map_between_coproduct_enriched ; cbn. apply is_binary_coprod_enriched_arrow_in1. + rewrite transportf_enriched_arr_r. rewrite idtoiso_isotoid. cbn. refine (_ @ enriched_from_to_arr E _). apply maponpaths. unfold map_between_coproduct_enriched ; cbn. apply is_binary_coprod_enriched_arrow_in2. 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.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Import MonoidalNotations. Section BinaryCoproductFromUnderlying. End BinaryCoproductFromUnderlying.