Def CategoryTheory.Functor.costructuredArrowMapCocone

Modification history

2024-10-04 11:14

Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

feat(CategoryTheory): lemmas about `descOfIsLeftKanExtension` for pointwise left Kan extensions (+dual) (#17383)

Added CategoryTheory.Functor.costructuredArrowMapCocone View on Github →