3 ms·

Thanks, and there is Subobject, which looks like the subobject classifier. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory

Thanks, and there is Subobject, which looks like the subobject classifier. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Subobject/Basic.lean https://github.com/leanprover-community/mathlib4/blob/master...

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