Proposition underlying_Coequalizer_arr_in {w : C} (h : y --> w) (q : f · h = g · h) : enriched_coequalizer_cocone_in a · underlying_Coequalizer_arr h q = h. Proof. unfold underlying_Coequalizer_arr, enriched_coequalizer_cocone_in. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E _ _))) ; cbn. rewrite enriched_from_arr_comp. rewrite !enriched_from_to_arr. refine (_ @ EqualizerCommutes (is_coequalizer_enriched_to_Equalizer Ha w) I_{V} (enriched_from_arr E h) _). rewrite tensor_split'. rewrite !assoc. rewrite mon_linvunitor_I_mon_rinvunitor_I. rewrite <- tensor_rinvunitor. cbn. unfold precomp_arr. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. do 3 apply maponpaths. refine (!_). apply enriched_from_to_arr. 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.