Lemma SubobjectClassifier_nt_is_nat_z_iso : is_nat_z_iso SubobjectClassifier_nat_trans. 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 global_element_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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Subobjects. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Subcategory.Core.