Definition Equalizers_in_HSET : Equalizers HSET. Proof. intros X Y f g ; cbn in *. simple refine ((_ ,, _) ,, _ ,, _). - exact (∑ (x : X), hProp_to_hSet (eqset (f x) (g x)))%set. - exact (λ x, pr1 x). - abstract (use funextsec ; intro z ; cbn ; exact (pr2 z)). - intros W h p. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; use funextsec ; intro w ; use subtypePath ; [ intro ; apply setproperty | ] ; exact (eqtohomot (pr2 φ₁ @ !(pr2 φ₂)) w)). + simple refine (_ ,, _). * exact (λ w, h w ,, eqtohomot p w). * 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.WeakEquivalences. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Categories.HSET.Core.