Proposition equalizer_enriched_from_underlying_map_inv₁ (h : I_{ V} --> E ⦃ w, a ⦄) : equalizer_enriched_from_underlying_map (h · equalizer_enriched_to_equalizer EqV a w) = h. Proof. unfold equalizer_enriched_from_underlying_map. refine (_ @ enriched_from_to_arr E h). apply maponpaths. use (isEqualizerInsEq eq_a). etrans. { apply (EqualizerCommutes (make_Equalizer _ _ _ _ eq_a)). } unfold enriched_equalizer_cone_pr. rewrite (enriched_to_arr_comp E). apply maponpaths. rewrite tensor_split. rewrite !assoc. rewrite <- tensor_linvunitor. rewrite enriched_from_to_arr. rewrite !assoc'. apply maponpaths. unfold equalizer_enriched_to_equalizer. rewrite EqualizerCommutes. rewrite !assoc. 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.