fact: Definition make_is_coequalizer_enriched (a : enriched_coequalizer_cocone) (eq_arr_eq : ∏ (w : C) (v : V) (h₁ h₂ : v --> E ⦃ a , w ⦄) (q : h₁ · precomp_arr E w (enriched_coequalizer_cocone_in a) = h₂ · precomp_arr E w (enriched_coequalizer_cocone_in a)), h₁ = h₂) (eq_in : ∏ (w : C) (v : V) (h : v --> E ⦃ y , w ⦄) (q : h · precomp_arr E w f = h · precomp_arr E w g), v --> E ⦃ a , w ⦄) (eq_in_eq : ∏ (w : C) (v : V) (h : v --> E ⦃ y , w ⦄) (q : h · precomp_arr E w f = h · precomp_arr E w g), eq_in w v h q · precomp_arr E w (enriched_coequalizer_cocone_in a) = h) : is_coequalizer_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 UniMath.CategoryTheory.Limits.Coequalizers