Theorem CategoryTheory.Presieve.isSheaf_comp_uliftFunctor

Modification history

2026-02-01 14:48
Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
chore(CategoryTheory/Sites): generalize universes in `Sheaf.isSheaf_of_isRepresentable` (#34234) …
Modified CategoryTheory.Presieve.isSheaf_comp_uliftFunctorView on Github →
2025-08-15 09:40
Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (#27816) …
Added CategoryTheory.Presieve.isSheaf_comp_uliftFunctorView on Github →