Proposition coequalizer_enriched_from_underlying_map_inv₂ (h : I_{V} --> EqV _ _ (precomp_arr E w f) (precomp_arr E w g)) : coequalizer_enriched_from_underlying_map h · coequalizer_enriched_to_equalizer EqV a w = h. Proof. unfold coequalizer_enriched_from_underlying_map. use (isEqualizerInsEq (pr22 (EqV _ _ _ _))). unfold coequalizer_enriched_to_equalizer. rewrite !assoc'. rewrite EqualizerCommutes. rewrite enriched_from_arr_precomp. refine (_ @ enriched_from_to_arr E _). apply maponpaths. apply (CoequalizerCommutes (make_Coequalizer _ _ _ _ eq_a)). 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.