Commit 2020-04-17 04:14 f3471479View on Github →
feat(category_theory): creation of limits and reflection of isomorphisms (#2426) Define creation of limits and reflection of isomorphisms. Part 2 of a sequence of PRs aiming to resolve my TODO here - that the forgetful functor from the over category creates connected limits. Remaining:
- Add an instance or def which gives that if
Fcreates limits and
K ⋙ F
has_limit Kas well.
- Move the forget creates limits proof to limits/over, and remove the existing proof since this one is strictly stronger - make sure to keep the statement there though using the previous point.
- Add more docstrings Probably relevant to @semorrison and @TwoFX.