Proposition is_subobject_classifier_eq_ar {C : category} {T : Terminal C} {O : C} {t t' : T --> O} (p : t = t') (H : is_subobject_classifier T O t) : is_subobject_classifier T O t'. Proof. pose (Ω := (O ,, t ,, H) : subobject_classifier T). intros x y m. use iscontraprop1. - abstract (use invproofirrelevance ; intros χ₁ χ₂ ; use subtypePath ; [ intro ; apply isaprop_is_subobject_classifier_arr | ] ; induction p ; exact (subobject_classifier_map_eq Ω m (pr12 χ₁) (pr12 χ₂) (pr22 χ₁) (pr22 χ₂))). - simple refine (_ ,, _ ,, _). + exact (characteristic_morphism Ω m). + abstract (rewrite <- p ; exact (subobject_classifier_square_commutes Ω m)). + cbn. use (isPullback_mor_paths _ _ _ _ _ _ (isPullback_Pullback (subobject_classifier_pullback Ω m))). * apply idpath. * exact p. * apply idpath. * apply idpath. 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.