Proposition postcomp_eq_from_equalizer_cone (a : enriched_equalizer_cone) (w : C) : postcomp_arr E w (enriched_equalizer_cone_pr a) · postcomp_arr E w f = postcomp_arr E w (enriched_equalizer_cone_pr a) · postcomp_arr E w g. Proof. rewrite <- !postcomp_arr_comp. apply maponpaths. apply enriched_equalizer_cone_eq. 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.