Proposition equalizer_enriched_from_underlying_map_inv₂ (h : I_{ V} --> EqV _ _ (postcomp_arr E w f) (postcomp_arr E w g)) : equalizer_enriched_from_underlying_map h · equalizer_enriched_to_equalizer EqV a w = h. Proof. unfold equalizer_enriched_from_underlying_map. use (isEqualizerInsEq (pr22 (EqV _ _ _ _))). unfold equalizer_enriched_to_equalizer. rewrite !assoc'. rewrite EqualizerCommutes. rewrite enriched_from_arr_postcomp. refine (_ @ enriched_from_to_arr E _). apply maponpaths. apply (EqualizerCommutes (make_Equalizer _ _ _ _ eq_a)). 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.