Proposition isaprop_Coequalizer {C : category} (HC : is_univalent C) {x y : C} (f g : x --> y) : isaprop (Coequalizer f g). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use (isaprop_total2 (_ ,, _) (λ _, (_ ,, _))). - apply homset_property. - simpl. repeat (use impred ; intro). apply isapropiscontr. } use total2_paths_f. - use (isotoid _ HC). use z_iso_between_Coequalizer. - rewrite transportf_isotoid' ; cbn. apply CoequalizerCommutes. 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.