Def CategoryTheory.shrinkYonedaIsoYoneda

Modification history

2026-03-13 23:21

Mathlib/CategoryTheory/ShrinkYoneda.lean

chore(CategoryTheory/Sites): generalize universes in `Presieve.isSheafFor_iff_yonedaSheafCondition` (#36461) …

Added CategoryTheory.shrinkYonedaIsoYoneda View on Github →