As others said above, `mathlib4` has quite a lot of Sheaf theory, and in particular the category of sheaves of Sets (i.e. Types) over an arbitrary site. In this sense, it is possible to talk about Grothendieck toposes.…
To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.
As others said above, `mathlib4` has quite a lot of Sheaf theory, and in particular the category of sheaves of Sets (i.e. Types) over an arbitrary site. In this sense, it is possible to talk about Grothendieck toposes.…
To clarify, this is not really related to subobject classifiers. This defines subobjects of `X` as equivalence classes of monomorphisms with target `X`.