Definition z_iso_to_Coequalizer {C : category} {x y c₂ : C} {f g : x --> y} (c₁ : Coequalizer f g) (h : z_iso c₁ c₂) : Coequalizer f g. Proof. use make_Coequalizer. - exact c₂. - exact (CoequalizerArrow c₁ · h). - abstract (rewrite !assoc ; rewrite CoequalizerEqAr ; apply idpath). - intros w k q. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; use (cancel_z_iso' h) ; use (isCoequalizerOutsEq (pr22 c₁)) ; rewrite !assoc ; exact (pr2 φ₁ @ !(pr2 φ₂))). + refine (inv_from_z_iso h · CoequalizerOut c₁ w k q ,, _). abstract (rewrite !assoc' ; rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)) ; rewrite z_iso_inv_after_z_iso ; rewrite id_left ; rewrite CoequalizerCommutes ; 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.