Proposition underlying_Equalizer_arr_eq {w : C} {h₁ h₂ : w --> a} (q : h₁ · enriched_equalizer_cone_pr a = h₂ · enriched_equalizer_cone_pr a) : h₁ = h₂. Proof. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. use (EqualizerInsEq (is_equalizer_enriched_to_Equalizer Ha w)). cbn. unfold postcomp_arr. rewrite !assoc. rewrite !tensor_linvunitor. rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- !tensor_split. use (invmaponpathsweq (make_weq _ (isweq_enriched_to_arr E _ _))) ; cbn. rewrite !assoc. rewrite <- !(enriched_to_arr_comp E). exact q. 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.