Def CategoryTheory.denseAtUliftYoneda

Modification history

2026-10-31 10:05

Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean

refactor(CategoryTheory): colimits of representable presheaves (#42816) …

Deleted CategoryTheory.denseAtUliftYoneda View on Github →

2026-05-26 05:31

Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean

chore(CategoryTheory/Functor): more API for dense functors (#39845) …

Added CategoryTheory.denseAtUliftYoneda View on Github →