fact: Definition make_is_equalizer_enriched (a : enriched_equalizer_cone) (eq_arr_eq : ∏ (w : C) (v : V) (h₁ h₂ : v --> E ⦃ w, a ⦄) (q : h₁ · postcomp_arr E w (enriched_equalizer_cone_pr a) = h₂ · postcomp_arr E w (enriched_equalizer_cone_pr a)), h₁ = h₂) (eq_in : ∏ (w : C) (v : V) (h : v --> E ⦃ w, x ⦄) (q : h · postcomp_arr E w f = h · postcomp_arr E w g), v --> E ⦃ w, a ⦄) (eq_in_eq : ∏ (w : C) (v : V) (h : v --> E ⦃ w, x ⦄) (q : h · postcomp_arr E w f = h · postcomp_arr E w g), eq_in w v h q · postcomp_arr E w (enriched_equalizer_cone_pr a) = h) : is_equalizer_enriched a.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.Limits.Equalizers