Definition make_is_coequalizer_enriched (a : enriched_coequalizer_cocone) (eq_arr_eq : ∏ (w : C) (v : V) (h₁ h₂ : v --> E ⦃ a , w ⦄) (q : h₁ · precomp_arr E w (enriched_coequalizer_cocone_in a) = h₂ · precomp_arr E w (enriched_coequalizer_cocone_in a)), h₁ = h₂) (eq_in : ∏ (w : C) (v : V) (h : v --> E ⦃ y , w ⦄) (q : h · precomp_arr E w f = h · precomp_arr E w g), v --> E ⦃ a , w ⦄) (eq_in_eq : ∏ (w : C) (v : V) (h : v --> E ⦃ y , w ⦄) (q : h · precomp_arr E w f = h · precomp_arr E w g), eq_in w v h q · precomp_arr E w (enriched_coequalizer_cocone_in a) = h) : is_coequalizer_enriched a. Proof. intro w. use make_isEqualizer. intros v h q. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; exact (eq_arr_eq w v _ _ (pr2 φ₁ @ !(pr2 φ₂)))). - exact (eq_in w v h q,, eq_in_eq w v h q). Defined.
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.