Proposition coequalizers_from_reflexive_eq : f · CoequalizerArrow coequalizers_from_reflexive_ob = g · CoequalizerArrow coequalizers_from_reflexive_ob. Proof. pose (maponpaths (λ z, BinCoproductIn1 _ · z) (CoequalizerEqAr coequalizers_from_reflexive_ob)) as p. unfold ℓ, ρ in p. unfold coequalizers_from_reflexive_left_map in p. unfold coequalizers_from_reflexive_right_map in p. rewrite !assoc in p. rewrite !BinCoproductIn1Commutes in p. exact p. 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.Epis. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Retracts. Section CoequalizersFromReflexiveCoequalizers. Section CoequalizersFromReflexive. End CoequalizersFromReflexive. End CoequalizersFromReflexiveCoequalizers.