Commit 2026-03-20 18:13 685b80af
View on Github →feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types (#35867)
This PR defines Sheaf.classifier J : Classifier (Sheaf J (Type (max u v)), which is the last ingredient missing to sheaf categories being elementary topoi.
adapted from:
https://github.com/edegeltje/CwFTT/blob/591d4505390172ae70e1bc97544d293a35cc0b3f/CwFTT/Classifier/Sheaf.lean