proposition: 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: 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.
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