feat(category_theory/limits): make has_limit a Prop (#3995)
We change `has_limit` so that it is only an existential statement that limit data exists, and in particular lives in `Prop`.
This means we can safely have multiple `has_limit` classes for the same functor, because proof irrelevance ensures Lean sees them all as the same.
We still have access to the API which lets us pretend we have consistently chosen limits, but now these limits are provided by the axiom of choice and hence are definitionally opaque.
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Simon Hudon <simon.hudon@gmail.com>
