CategoryTheory.Limits.IsLimit not in Prop

Stream: mathlib4

[Yury G. Kudryashov]

I accidentally found out (I don't usually use this part of the library) that docs#CategoryTheory.Limits.IsLimit (and all the typeclasses defined in terms of this one) is not a Prop. It would be nice if someone who is more familiar with category theory in Mathlib will expand the docstring to explain that this has Is prefix but is not a Prop, so the users should be careful. Also, it would be nice to add similar comments to typeclasses like PreservesLimitsOfShape.

[Yury G. Kudryashov]

Pinging @Scott Morrison, the author of this file.

[Adam Topaz]

IsLimit should definitely not be a prop. OTOH one could argue that PreservesLimitsOfShape and friends should be a prop

[Adam Topaz]

IMO, This is one case where the prefix “Is” does make sense, even though the structure contains data

[Yury G. Kudryashov]

I don't claim that it should be a Prop. I claim that the fact that it's not a Prop should be explained in the docstring.

[Kevin Buzzard]

docs#IsROrC

[Kevin Buzzard]

You're familiar with that part of the library :P

[Yury G. Kudryashov]

Thanks, I'll expand this docstring soon!

[Yury G. Kudryashov]

#10444 ?

[Yury G. Kudryashov]

Wait a minute, I'll add more.

[Yury G. Kudryashov]

Done.