Proposition isaprop_enrichment_coequalizers {V : monoidal_cat} {C : category} (HC : is_univalent C) (E : enrichment C V) : isaprop (enrichment_coequalizers E). Proof. use invproofirrelevance. intros φ₁ φ₂. use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro f. use funextsec ; intro g. use subtypePath. { intro. apply isaprop_is_coequalizer_enriched. } use total2_paths_f. - use (isotoid _ HC). use iso_between_coequalizer_enriched. + exact (pr2 (φ₁ x y f g)). + exact (pr2 (φ₂ x y f g)). - use subtypePath. { intro. apply homset_property. } rewrite pr1_transportf. rewrite transportf_enriched_arr_r. rewrite idtoiso_isotoid. cbn. refine (_ @ enriched_from_to_arr E _). apply maponpaths. unfold map_between_coequalizer_enriched ; cbn. apply underlying_Coequalizer_arr_in. 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.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Import MonoidalNotations. Section CoequalizersFromUnderlying. End CoequalizersFromUnderlying.