Lemma iso_between_coequalizer_enriched_inv {a b : enriched_coequalizer_cocone} (Ha : is_coequalizer_enriched a) (Hb : is_coequalizer_enriched b) : map_between_coequalizer_enriched Ha Hb · map_between_coequalizer_enriched Hb Ha = identity _. Proof. unfold map_between_coequalizer_enriched. use (underlying_Coequalizer_arr_eq Ha). rewrite !assoc. rewrite !underlying_Coequalizer_arr_in. rewrite id_right. 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.