Commit 2023-08-26 19:18 f8d81046
View on Github →feat(CategoryTheory/Bicategory): define left Kan extensions (#6552)
The basic design follows the API for colimits in the category theory library.
The dictionary looks like:
Current PR
LeftExtension <-> Limits.Cocone
LeftExtension.IsKan <-> Limits.IsColimit
Future PR
LeftExtension.HasKan <-> Limits.HasColimit
lan <-> Limits.colimit
The diagrams in the docs are far from ideal, but I hope it helps for the time being. I would be very happy to have a graphical visualization by e.g. the widgets.