Commit 2021-01-12 07:23 cd0d8c02

chore(category_theory/limits/over): generalise, golf and document over limits (#5674)

• Show that the forgetful functor over X => C creates colimits, generalising what was already there
• Golf the proofs using this new instance
• Add module doc and duals of the above