Lemma PullbacksHSET : Pullbacks HSET. 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.
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.