Definition enriched_equalizer_cone_from_iso : enriched_equalizer_cone. Proof. refine (make_enriched_equalizer_cone b (enriched_from_arr E (h · enriched_equalizer_cone_pr a)) _). abstract (rewrite !enriched_to_from_arr ; rewrite !assoc' ; apply maponpaths ; exact (enriched_equalizer_cone_eq a)). 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.