Definition identity_preserves_subobject_classifier {C : category} (T : Terminal C) : preserves_subobject_classifier (functor_identity C) T T (identity_preserves_terminal C). Proof. intros Ω t H. use (is_subobject_classifier_eq_ar _ H). abstract (cbn ; refine (!(id_left _) @ _) ; apply maponpaths_2 ; apply TerminalArrowEq). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso.