Def CategoryTheory.Functor.Elements.uliftYonedaCocone

Modification history

2026-10-31 10:05

Mathlib/CategoryTheory/Functor/KanExtension/DenseAtYoneda.lean

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

Added CategoryTheory.Functor.Elements.uliftYonedaCocone View on Github →