Lemma CoequalizerOutComp {y z : C} {f g : y --> z} (CE : Coequalizer f g) {w w' : C} (h1 : z --> w) (h2 : w --> w') (H1 : f · (h1 · h2) = g · (h1 · h2)) (H2 : f · h1 = g · h1) : CoequalizerOut CE w' (h1 · h2) H1 = CoequalizerOut CE w h1 H2 · h2. Proof. use CoequalizerOutsEq. rewrite CoequalizerCommutes. rewrite assoc. rewrite CoequalizerCommutes. apply idpath. 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.