Proposition mor_subobject_classifier_inv {C : category} {T : Terminal C} (Ω Ω' : subobject_classifier T) : mor_subobject_classifier Ω Ω' · mor_subobject_classifier Ω' Ω = identity Ω. Proof. use subobject_classifier_map_eq. - exact T. - exact (true Ω). - abstract (cbn ; unfold mor_subobject_classifier ; rewrite !assoc ; refine (maponpaths (λ z, z · _) (subobject_classifier_square_commutes Ω' (true Ω)) @ _) ; rewrite assoc' ; refine (maponpaths (λ z, _ · z) (subobject_classifier_square_commutes Ω (true Ω')) @ _) ; unfold const_true ; cbn ; rewrite !assoc ; apply maponpaths_2 ; apply TerminalArrowEq). - abstract (unfold const_true ; rewrite id_right ; refine (!(id_left _) @ _) ; apply maponpaths_2 ; apply TerminalArrowEq). - use (isPullback_mor_paths _ _ _ _ _ _ (isPullback_Pullback (pullback_glue_pullback _ (subobject_classifier_pullback Ω (true Ω')) (subobject_classifier_pullback Ω' (true Ω))))). + apply idpath. + apply idpath. + apply idpath. + apply TerminalArrowEq. - use (isPullback_mor_paths _ _ _ _ _ _ (isPullback_Pullback (subobject_classifier_pullback Ω (true Ω)))). + apply characteristic_morphism_true. + apply idpath. + apply idpath. + apply idpath. Qed.
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.Monics. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier.