Def CategoryTheory.OverPresheafAux.restrictedYoneda

Modification history

2026-04-14 15:27
Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
refactor(CategoryTheory): one-field structure morphisms in the category of types (#36613) …
Modified CategoryTheory.OverPresheafAux.restrictedYonedaView on Github →
2024-02-13 09:59
Mathlib/CategoryTheory/Comma/Presheaf.lean
feat: computation of `Over A` for a presheaf `A` (#10245)
Added CategoryTheory.OverPresheafAux.restrictedYonedaView on Github →