Proposition underlying_Equalizer_arr_pr {w : C} (h : w --> x) (q : h · f = h · g) : underlying_Equalizer_arr h q · enriched_equalizer_cone_pr a = h. Proof. unfold underlying_Equalizer_arr, enriched_equalizer_cone_pr. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E _ _))) ; cbn. rewrite enriched_from_arr_comp. rewrite !enriched_from_to_arr. rewrite tensor_split. rewrite !assoc. rewrite <- tensor_linvunitor. rewrite !assoc'. refine (maponpaths (λ z, _ · z) _ @ EqualizerCommutes (is_equalizer_enriched_to_Equalizer Ha w) I_{V} (enriched_from_arr E h) _). cbn ; unfold postcomp_arr. rewrite !assoc'. apply maponpaths. do 2 apply maponpaths_2. refine (!_). apply enriched_from_to_arr. 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.