Definition make_subobject_classifier {C : category} {T : Terminal C} (O : ob C) (true : C⟦T, O⟧) : (∏ (X Y : ob C) (m : Monic _ X Y), iscontr (∑ (chi : C⟦Y, O⟧) (H : m · chi = TerminalArrow _ _ · true), isPullback H)) -> subobject_classifier T.
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.