proposition: Proposition coequalizers_from_reflexive_eq : f · CoequalizerArrow coequalizers_from_reflexive_ob = g · CoequalizerArrow coequalizers_from_reflexive_ob.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Retracts