Definition make_is_coequalizer_enriched_from_z_iso (EqV : Equalizers V) (a : enriched_coequalizer_cocone) (Ha : ∏ (w : C), is_z_isomorphism (coequalizer_enriched_to_equalizer EqV a w)) : is_coequalizer_enriched a. Proof. intro w. use (isEqualizer_z_iso (pr22 (EqV _ _ (precomp_arr E w f) (precomp_arr E w g))) (_ ,, Ha w)). abstract (unfold coequalizer_enriched_to_equalizer ; cbn ; refine (!_) ; apply EqualizerCommutes). 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.