Commit 2020-09-12 06:00 34199869View on Github →
feat(category_theory/limits): make has_limit a Prop (#3995)
has_limit so that it is only an existential statement that limit data exists, and in particular lives in
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.