Theorem CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamation

Modification history

2026-03-13 23:21
Mathlib/CategoryTheory/Sites/IsSheafFor.lean
chore(CategoryTheory/Sites): generalize universes in `Presieve.isSheafFor_iff_yonedaSheafCondition` (#36461) …
Added CategoryTheory.Presieve.shrinkFunctor_ι_comp_eq_iff_isAmalgamationView on Github →