Definition coequalizer_enriched_from_underlying_map (h : I_{V} --> EqV _ _ (precomp_arr E w f) (precomp_arr E w g)) : I_{V} --> E ⦃ a , w ⦄. Proof. use enriched_from_arr. use (CoequalizerOut (make_Coequalizer _ _ _ _ eq_a)). - exact (enriched_to_arr E (h · EqualizerArrow _)). - abstract (use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E _ _))) ; cbn ; rewrite !enriched_from_arr_comp ; rewrite !enriched_from_to_arr ; rewrite tensor_split' ; rewrite !assoc ; rewrite !mon_linvunitor_I_mon_rinvunitor_I ; rewrite <- !tensor_rinvunitor ; rewrite !assoc' ; rewrite !(maponpaths (λ z, _ · (_ · z)) (assoc _ _ _)) ; refine (maponpaths (λ z, _ · z) (EqualizerEqAr (EqV _ _ (precomp_arr E w f) (precomp_arr E w g))) @ _) ; refine (!_) ; rewrite tensor_split' ; rewrite !assoc ; rewrite <- tensor_rinvunitor ; rewrite !assoc' ; do 2 apply maponpaths ; unfold precomp_arr ; rewrite !assoc' ; apply idpath). Defined.
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.