generalnonsense
No user record in our sample, but generalnonsense has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
No user record in our sample, but generalnonsense has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
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`.