Commit 2020-12-02 19:13 0bb88094

feat(category_theory/limits): left adjoint if preserves colimits (#4942) A slight generalisation of a construction from before. Maybe this is the dual version you were talking about @jcommelin - if so my mistake! I think the advantage of doing it this way is that you definitionally get the old version but also the new version too.