Definition Coequalizers_HSET : Coequalizers HSET. Proof. intros X Y f g. use make_Coequalizer. - exact (coequalizer_hSet f g). - exact (coequalizer_map_hSet f g). - abstract (use funextsec ; intro x ; cbn ; exact (coequalizer_eq_hSet f g x)). - intros Z h p. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; use funextsec ; use setquotunivprop' ; [ intro ; apply setproperty | ] ; intro x ; cbn ; exact (eqtohomot (pr2 φ₁ @ !(pr2 φ₂)) x)). + simple refine (_ ,, _). * exact (coequalizer_out_hSet f g h (eqtohomot p)). * abstract (apply idpath). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Coproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.MoreFoundations.Subtypes.