Proposition underlying_Coequalizer_arr_eq {w : C} {h₁ h₂ : a --> w} (q : enriched_coequalizer_cocone_in a · h₁ = enriched_coequalizer_cocone_in a · h₂) : h₁ = h₂. Proof. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. use (EqualizerInsEq (is_coequalizer_enriched_to_Equalizer Ha w)). cbn. unfold precomp_arr. rewrite !assoc. rewrite !tensor_rinvunitor. rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). rewrite <- !tensor_split'. use (invmaponpathsweq (make_weq _ (isweq_enriched_to_arr E _ _))) ; cbn. rewrite !assoc. rewrite mon_rinvunitor_I_mon_linvunitor_I. rewrite <- !(enriched_to_arr_comp E). exact q. 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.