Proposition coequalizer_enriched_from_underlying_map_inv₁ (h : I_{V} --> E ⦃ a , w ⦄) : coequalizer_enriched_from_underlying_map (h · coequalizer_enriched_to_equalizer EqV a w) = h. Proof. unfold coequalizer_enriched_from_underlying_map. refine (_ @ enriched_from_to_arr E h). apply maponpaths. use (isCoequalizerOutsEq eq_a). etrans. { apply (CoequalizerCommutes (make_Coequalizer _ _ _ _ eq_a)). } unfold enriched_coequalizer_cocone_in. rewrite (enriched_to_arr_comp E). apply maponpaths. rewrite tensor_split'. rewrite !assoc. rewrite mon_linvunitor_I_mon_rinvunitor_I. rewrite <- tensor_rinvunitor. rewrite enriched_from_to_arr. rewrite !assoc'. apply maponpaths. unfold coequalizer_enriched_to_equalizer. rewrite EqualizerCommutes. rewrite !assoc. apply idpath. 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.