Proposition precomp_eq_from_coequalizer_cocone (a : enriched_coequalizer_cocone) (w : C) : precomp_arr E w (enriched_coequalizer_cocone_in a) · precomp_arr E w f = precomp_arr E w (enriched_coequalizer_cocone_in a) · precomp_arr E w g. Proof. rewrite <- !precomp_arr_comp. apply maponpaths. apply enriched_coequalizer_cocone_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. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Import MonoidalNotations. Section CoequalizersFromUnderlying. End CoequalizersFromUnderlying.