proposition: Lemma carrier_Pullback {Y : HSET} (chi : HSET ⟦ Y, hProp_set ⟧) : Pullback chi (@const_htrue unitHSET).
proof: Proof. use make_Pullback. - exact (carrier_subset chi). - exact (pr1carrier _). - exact (TerminalArrow TerminalHSET _). - apply funextfun; intro yy. apply hProp_eq_unit; cbn. apply (pr2 yy). - cbn. intros pb' h k H. use make_iscontr. + use tpair. * intro p. use tpair. -- exact (h p). -- apply toforallpaths in H; cbn. specialize (H p); cbn in H. abstract (rewrite H; exact tt). * split; [apply idpath|]. apply proofirrelevance, hlevelntosn, iscontrfuntounit. + intro t. apply subtypePath; [intro; apply isapropdirprod; apply isaset_set_fun_space|]. apply funextfun; intro. apply subtypePath; [intro; apply propproperty|]. refine (_ @ toforallpaths _ _ _ (pr1 (pr2 t)) x). apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.AxiomOfChoice UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.NNO UniMath.CategoryTheory.SubobjectClassifier UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Categories.Type.MonoEpiIso UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.covyoneda UniMath.CategoryTheory.EpiFacts UniMath.CategoryTheory.Monics UniMath.CategoryTheory.SplitMonicsAndEpis UniMath.CategoryTheory.ElementaryTopos UniMath.CategoryTheory.PowerObject UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.Categories.HSET.Univalence