Definition subobject_classifier_HSET_pullback {X Y : HSET} (m : Monic HSET X Y) : ∑ (chi : HSET ⟦ Y, hProp_set ⟧) (H : m · chi = TerminalArrow TerminalHSET X · const_htrue), isPullback H. Proof. exists (fun z => (hfiber (pr1 m) z,, isaprop_hfiber_monic (pr1 m) (pr2 m) z)). use tpair. + apply funextfun; intro. apply hProp_eq_unit; cbn. use make_hfiber. * assumption. * apply idpath. + cbn beta. unfold isPullback; cbn. intros Z f g H. use make_iscontr. * use tpair. -- intro z. eapply hfiberpr1. eapply eqweqmap. ++ apply pathsinv0. apply (maponpaths pr1 (toforallpaths _ _ _ H z)). ++ exact tt. -- split. ++ apply funextfun; intro z; cbn. apply hfiberpr2. ++ apply proofirrelevance, impred. intro; apply isapropunit. * intro t. apply subtypePath. -- intro. apply isapropdirprod. ++ apply funspace_isaset, setproperty. ++ apply funspace_isaset, isasetunit. -- cbn. apply funextsec; intro; cbn. apply (invweq (make_weq _ (MonosAreInjective_HSET m (MonicisMonic _ m) _ _))). eapply pathscomp0. ++ apply (toforallpaths _ _ _ (pr1 (pr2 t))). ++ apply pathsinv0. apply hfiberpr2. 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).