proposition: Lemma SubobjectClassifier_nt_is_nat_z_iso : is_nat_z_iso SubobjectClassifier_nat_trans.
proof: Proof. intros c. use make_is_z_isomorphism. + intro phi. cbn in c, phi. use setquotpr. use (PullbackSubobject PB _ phi). use (Subobjectscategory_ob (true O)). apply from_terminal_isMonic. + use make_is_inverse_in_precat. - use funextfun. intro S. use (squash_to_prop (X:= pr1setquot _ S) ((eqax0 (SubObj_iseqc S)))). { use isasetsetquot. } intro m. induction (setquotl0 _ _ m). use weqpathsinsetquot. use hinhpr. cbn. set (pbc := subobject_classifier_pullback O ((Subobject_Monic (pr1carrier _ m)))). set (PBc := PB _ _ _ (characteristic_morphism O (Subobject_Monic (pr1carrier _ m))) O). induction (pullbackiso _ PBc pbc) as (PBpb_z_iso,(PBpb_z_iso1,PBpb_z_iso2)). use make_z_iso_in_Subobjectscategory. * cbn. exact PBpb_z_iso. * use z_iso_is_z_isomorphism. * apply pathsinv0. exact PBpb_z_iso1. - use funextfun. intro phi. cbn. apply pathsinv0. use path_to_ctr. cbn. set (pb := PB O c T phi (true' O)). use (isPullback_mor_paths' _ _ _ _ _ (isPullback_Pullback pb)). * apply idpath. * apply idpath. * apply idpath. * use TerminalArrowUnique. Defined.
imports: UniMath.Foundations.PartA UniMath.Foundations.PartB UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Subobjects UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Core.Functors UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Subcategory.Core