[hiker]

There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2]

[1] https://github.com/leanprover-community/mathlib4/tree/master...

[2] https://leanprover-community.github.io/blog/posts/lte-final/

[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`.