Definition SubobjectClassifier_nt_data : nat_trans_data (SubObj_Functor C PB) (contra_homSet_functor O). Proof. intros c S. cbn in c. change (pr1hSet (SubObj c)) in S. cbn. use (squash_to_set (X:=(pr1setquot (z_iso_eqrel (C:=Subobjectscategory c)) S))). + use homset_property. + intro m. exact (characteristic_morphism O (Subobject_Monic (pr1carrier _ m))). + intros m m'. cbn. assert (ej : (z_iso_eqrel (C:=Subobjectscategory c)) (pr1carrier _ m') (pr1carrier _ m)). { use (invweq (weqpathsinsetquot _ _ _)). use (pathscomp0 (b:=S)). * use (setquotl0 (z_iso_eqrel (C:=Subobjectscategory c))). * use pathsinv0. use (setquotl0 (z_iso_eqrel (C:=Subobjectscategory c))). } use (squash_to_prop ej). - use homset_property. - intro j. use path_to_ctr. cbn. transparent assert (pb_aux : (Pullback ((identity c)·(characteristic_morphism O (Subobject_Monic (pr1carrier _ m)))) (true' O))). { use (Pullback_z_iso_of_morphisms). * exact (subobject_classifier_pullback O (Subobject_Monic (pr1carrier _ m))). * exact (Subobject_dom (pr1carrier _ m')). * exact (z_iso_from_z_iso_in_Subobjectcategory j). * exact (Subobject_mor (pr1carrier _ m')). * exact (identity_is_z_iso c). * use z_iso_is_z_isomorphism. * rewrite id_right. use (Subobjectmor_tri j). } use (isPullback_mor_paths' _ _ _ _ _ (isPullback_Pullback pb_aux)). * rewrite id_left. apply idpath. * apply idpath. * apply idpath. * use TerminalArrowUnique. + exact (eqax0 (SubObj_iseqc S)). 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.