Definition z_iso_between_Coequalizer {C : category} {x y : C} {f g : x --> y} (c₁ c₂ : Coequalizer f g) : z_iso c₁ c₂. Proof. use make_z_iso. - exact (CoequalizerOut c₁ c₂ (CoequalizerArrow c₂) (CoequalizerEqAr c₂)). - exact (CoequalizerOut c₂ c₁ (CoequalizerArrow c₁) (CoequalizerEqAr c₁)). - split. + abstract (use (isCoequalizerOutsEq (pr22 c₁)) ; rewrite id_right ; rewrite !assoc ; rewrite !CoequalizerCommutes ; apply idpath). + abstract (use (isCoequalizerOutsEq (pr22 c₂)) ; rewrite id_right ; rewrite !assoc ; 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.