Lemma SubobjectClassifier_nt_is : is_nat_trans (SubObj_Functor C PB) (contra_homSet_functor O) SubobjectClassifier_nt_data. 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.
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.