proposition: Lemma SubobjectClassifier_nt_is : is_nat_trans (SubObj_Functor C PB) (contra_homSet_functor O) SubobjectClassifier_nt_data.
proof: Proof. intros c c' f. cbn in c, c', f. use funextfun. intro S. use (squash_to_prop (X := pr1setquot _ S)). + exact (eqax0 (SubObj_iseqc S)). + use homset_property. + intro m. induction (setquotl0 _ _ m). cbn. rewrite id_right. use pathsinv0. use path_to_ctr. set (pbr := subobject_classifier_pullback O (Subobject_Monic (pr1carrier _ m))). cbn. set (pbl := PB c c' (Subobject_dom (pr1carrier _ m)) f (Subobject_mor (pr1carrier _ m))). transparent assert (pb_glued : (Pullback (f·(characteristic_morphism O (Subobject_Monic (pr1carrier _ m)))) O)). { use make_Pullback. - exact pbl. - exact (PullbackPr1 pbl). - exact ((PullbackPr2 pbl)·(PullbackPr2 pbr)). - use glueSquares. * exact (PullbackPr1 pbr). * exact (PullbackSqrCommutes pbr). * exact (PullbackSqrCommutes pbl). - use (isPullbackGluedSquare (isPullback_Pullback pbr) (isPullback_Pullback pbl)). } use (isPullback_mor_paths' _ _ _ _ _ (isPullback_Pullback pb_glued)). - 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