Definition make_is_coequalizer_enriched_from_underlying (EqV : Equalizers V) (a : enriched_coequalizer_cocone) (eq_a : isCoequalizer f g (enriched_coequalizer_cocone_in a) (enriched_coequalizer_cocone_eq a)) (HV : conservative_moncat V) : is_coequalizer_enriched a. Proof. use (make_is_coequalizer_enriched_from_z_iso EqV). intros w. use HV. use isweq_iso. - exact (coequalizer_enriched_from_underlying_map EqV a eq_a w). - exact (coequalizer_enriched_from_underlying_map_inv₁ EqV a eq_a w). - exact (coequalizer_enriched_from_underlying_map_inv₂ EqV a eq_a w). 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.