[hackandthink]

Thanks,

and there is Subobject, which looks like the subobject classifier.

https://github.com/leanprover-community/mathlib4/blob/master...

[generalnonsense]

To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.