Lemma isiso_from_Coequalizer_to_Coequalizer {y z : C} {f g : y --> z} (E E' : Coequalizer f g) : is_iso (from_Coequalizer_to_Coequalizer E E'). Proof. apply (is_iso_qinv _ (from_Coequalizer_to_Coequalizer E' E)). apply are_inverses_from_Coequalizer_to_Coequalizer. 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.