Definition enrichment_equalizers {V : monoidal_cat} {C : category} (E : enrichment C V) : UU := ∏ (x y : C) (f g : x --> y), ∑ (a : enriched_equalizer_cone E f g), is_equalizer_enriched E f g a.
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.