Lemma carrier_Pullback {Y : HSET} (chi : HSET ⟦ Y, hProp_set ⟧) : Pullback chi (@const_htrue unitHSET). 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Categories.Type.MonoEpiIso. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.SplitMonicsAndEpis. Require Import UniMath.CategoryTheory.ElementaryTopos. Require Import UniMath.CategoryTheory.PowerObject. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. assert (p : (BinProductsFromPullbacks PullbacksHSET TerminalHSET) = BinProductsHSET).