Definition coequalizer_from_reflexive_ump : coequalizers_from_reflexive_ob --> z. Proof. use (CoequalizerOut coequalizers_from_reflexive_ob z h). abstract (use BinCoproductArrowsEq ; unfold ℓ, ρ ; unfold coequalizers_from_reflexive_left_map ; unfold coequalizers_from_reflexive_right_map ; rewrite !assoc ; rewrite ?BinCoproductIn1Commutes ; rewrite ?BinCoproductIn2Commutes ; [ exact p | 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.