Commit 2020-04-17 04:14 f3471479

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 F creates limits and K ⋙ F has_limit then has_limit K as 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.