Lemma hfiber_is_pullback {X Y : hSet} (f : HSET⟦X, Y⟧) (y : Y) (y' := invweq (weqfunfromunit_HSET _) y) : ∑ H, @isPullback _ _ _ _ _ f y' (hfiberpr1 f y : HSET⟦hfiber_hSet f y , X⟧) (TerminalArrow TerminalHSET _) H. Proof. use tpair. - apply funextfun; intro. apply hfiberpr2. - intros pb pbpr1 pbpr2 pbH. use iscontrweqb. + exact (∑ hk : HSET ⟦ pb, hfiber_hSet f y ⟧, hk · hfiberpr1 f y = pbpr1). + apply weqfibtototal; intro. apply invweq. apply dirprod_with_contr_r. use make_iscontr. * apply isapropifcontr. apply TerminalHSET. * intro; apply proofirrelevance; apply homset_property. + unfold hfiber_hSet, hfiber; cbn. use make_iscontr. * use tpair. intros pb0. use tpair. -- exact (pbpr1 pb0). -- cbn. apply toforallpaths in pbH. specialize (pbH pb0); cbn in pbH. refine (pbH @ _). apply tosecoverunit_compute. -- apply idpath. * intros t. apply subtypePath. -- intro; apply has_homsets_HSET. -- cbn. apply funextfun; intro; cbn. apply subtypePath. ++ intro; apply setproperty. ++ apply (toforallpaths _ _ _ (pr2 t)). 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.