Definition coequalizer_from_reflexive : Coequalizer f g. Proof. use make_Coequalizer. - exact coequalizers_from_reflexive_ob. - exact (CoequalizerArrow coequalizers_from_reflexive_ob). - exact coequalizers_from_reflexive_eq. - intros z h p. use iscontraprop1. + exact (coequalizer_from_reflexive_unique h). + simple refine (_ ,, _). * exact (coequalizer_from_reflexive_ump h p). * exact (coequalizer_from_reflexive_ump_eq h p). 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.