Definition iso_between_equalizer_enriched {a b : enriched_equalizer_cone} (Ha : is_equalizer_enriched a) (Hb : is_equalizer_enriched b) : z_iso a b. Proof. use make_z_iso. - exact (map_between_equalizer_enriched Ha Hb). - exact (map_between_equalizer_enriched Hb Ha). - split. + apply iso_between_equalizer_enriched_inv. + apply iso_between_equalizer_enriched_inv. 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.