Lemma iso_between_equalizer_enriched_inv {a b : enriched_equalizer_cone} (Ha : is_equalizer_enriched a) (Hb : is_equalizer_enriched b) : map_between_equalizer_enriched Ha Hb · map_between_equalizer_enriched Hb Ha = identity _. Proof. unfold map_between_equalizer_enriched. use (underlying_Equalizer_arr_eq Ha). rewrite !assoc'. rewrite !underlying_Equalizer_arr_pr. rewrite id_left. apply idpath. Qed.
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.