Definition subobject_classifier_map_eq {C : category} {T : Terminal C} (Ω : subobject_classifier T) {x y : C} (m : Monic C x y) {χ₁ χ₂ : y --> Ω} (p₁ : m · χ₁ = const_true x Ω) (p₂ : m · χ₂ = const_true x Ω) (H₁ : isPullback p₁) (H₂ : isPullback p₂) : χ₁ = χ₂.
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.