Commit 2020-09-12 06:00 34199869

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.