Lemma are_inverses_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z} {E E': Coequalizer f g} : is_inverse_in_precat (from_Coequalizer_to_Coequalizer E E') (from_Coequalizer_to_Coequalizer E' E). Proof. split; apply pathsinv0; use CoequalizerEndo_is_identity; rewrite assoc; unfold from_Coequalizer_to_Coequalizer; repeat rewrite CoequalizerCommutes; 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.Epis. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Retracts. Section CoequalizersFromReflexiveCoequalizers. Section CoequalizersFromReflexive. End CoequalizersFromReflexive. End CoequalizersFromReflexiveCoequalizers.