Commit 2026-05-26 05:31 7ba9e81f
View on Github →chore(CategoryTheory/Functor): more API for dense functors (#39845)
Given a dense functor F : C ⥤ D, we provide an isomorphism F.leftKanExtension F ≅ 𝟭 D. We also provide the instance that yoneda is dense.