Definition is_coequalizer_enriched_from_iso : is_coequalizer_enriched enriched_coequalizer_cocone_from_iso. Proof. intros w. use (isEqualizer_z_iso (Ha w)). - exact (precomp_arr_z_iso E w h). - abstract (cbn ; rewrite <- precomp_arr_comp ; apply maponpaths ; unfold enriched_coequalizer_cocone_from_iso ; cbn ; unfold enriched_coequalizer_cocone_in ; cbn ; rewrite enriched_to_from_arr ; apply idpath). 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.