Definition subobject_classifier_HSET : subobject_classifier TerminalHSET. Proof. exists hProp_set. exists const_htrue. intros X Y m. use make_iscontr. - apply subobject_classifier_HSET_pullback. - intro O'. apply subtypePath. + intro. apply Propositions.isaproptotal2. * intro; apply isaprop_isPullback. * intros; apply proofirrelevance, homset_property. + assert (eq : m · pr1 O' ~ m · (fun z => (hfiber (pr1 m) z,, isaprop_hfiber_monic (pr1 m) (pr2 m) z : pr1hSet hProp_set))). { apply toforallpaths. refine (pr1 (pr2 O') @ _). apply (!pr1 (pr2 (subobject_classifier_HSET_pullback m))). } apply funextfun; intro y. apply weqtopathshProp, weqimplimpl. * intro isO. pose (PBO' := make_Pullback (pr1 (pr2 O')) (pr2 (pr2 O'))). pose (PBC := carrier_Pullback (pr1 O')). pose (pbiso := pullbackiso _ PBC PBO'). use make_hfiber. -- exact (morphism_from_z_iso _ _ (pr1 pbiso) (y,, isO)). -- change (pr1 m (morphism_from_z_iso _ _ (pr1 pbiso) (y,, isO))) with (((pr1 pbiso) · pr1 m) (y,, isO)). change (pr1 m) with (PullbackPr1 PBO'). pose (pr1 (pr2 pbiso)) as p. exact (maponpaths (λ z, z _) p). * intros fib. apply (eqweqmap (maponpaths pr1 (maponpaths (pr1 O') (pr2 fib)))). apply (eqweqmap (maponpaths pr1 (eq (hfiberpr1 _ _ fib)))). apply hfiber_in_hfiber. * apply propproperty. * apply propproperty. 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).