Definition is_equalizer_enriched_from_iso : is_equalizer_enriched enriched_equalizer_cone_from_iso. Proof. intros w. use (isEqualizer_z_iso (Ha w)). - exact (postcomp_arr_z_iso E w h). - abstract (cbn ; rewrite <- postcomp_arr_comp ; apply maponpaths ; unfold enriched_equalizer_cone_from_iso ; cbn ; unfold enriched_equalizer_cone_pr ; 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. Import MonoidalNotations. Section EqualizersFromUnderlying. End EqualizersFromUnderlying.