proposition: Lemma PullbacksHSET : Pullbacks HSET.
proof: Proof. intros A B C f g. use make_Pullback. + apply (PullbackHSET_ob f g). + intros xy; apply (pr1 (pr1 xy)). + intros xy; apply (pr2 (pr1 xy)). + abstract (apply funextsec; intros [[x y] Hxy]; apply Hxy). + use make_isPullback. intros X f1 f2 Hf12; cbn. use unique_exists. - intros x. exists (f1 x,,f2 x); abstract (apply (toforallpaths _ _ _ Hf12)). - abstract (now split). - abstract (now intros h; apply isapropdirprod; apply has_homsets_HSET). - abstract (intros h [H1 H2]; apply funextsec; intro x; apply subtypePath; [intros H; apply setproperty|]; simpl; now rewrite <- (toforallpaths _ _ _ H1 x), <- (toforallpaths _ _ _ H2 x)). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.WeakEquivalences UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Equalizers UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Categories.HSET.Core