Proposition characteristic_morphism_true {C : category} {T : Terminal C} (Ω : subobject_classifier T) : characteristic_morphism Ω (true Ω) = identity _. Proof. refine (!_). use (maponpaths pr1 (pr2 (subobject_classifier_universal_property Ω (true Ω)) (_ ,, _ ,, _))). - abstract (refine (id_right _ @ !(id_left _) @ _) ; unfold true' ; cbn ; apply maponpaths_2 ; apply TerminalArrowEq). - use identity_isPullback. + apply idpath. + apply TerminalArrowEq. + apply idpath. Qed.
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.