Theorem CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iff

Modification history

2026-02-01 14:48
Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
chore(CategoryTheory/Sites): generalize universes in `Sheaf.isSheaf_of_isRepresentable` (#34234) …
Added CategoryTheory.Presieve.isSheaf_comp_uliftFunctor_iffView on Github →