Limits.IsLimit or Limits.UnivLimit

Stream: mathlib4

[Filippo A. E. Nuccio]

I'm a bit perplexed by the naming of docs#CategoryTheory.Limits.IsLimit, because it is not Prop-valued. Wouldn'it nicer to call this structure a UniversalLimitCone (or something) and have a IsLimitCone structure (Prop-valued, this time) by quantifying over all lifts and then either bundling fac and uniq in an and field (so, a one-field structure), or a two-field (both Prop-valued) structure, the fields being fac and uniq?

[Christian Merten]

The reasoning here is that it is a Subsingleton. The fact that IsLimit contains data rarely (never?) causes trouble.

[Filippo A. E. Nuccio]

The "trouble" I'm thinking of is psychological rather than anything else; it seems strange to start constructing a term in a IsFoo structure by producing a data for every s : Cone F. Are there other examples in the Category theory library (I don't know it well) where IsFoo structures appear although they contain data?

[Christian Merten]

I agree that IsLimit would probably not be the name we would choose if we had to choose a new name now. We have been following the Is-only-for-Props rule for new declarations for a while now, but renaming IsLimit would be a very annoying refactor, because it is used everywhere in the category theory library.

[Filippo A. E. Nuccio]

Is it really hard if we want to rename IsLimit to UnivLimit (say?). Given there's no namespace involved, I would imagine that we can quite easily search-and-replace, no?

[Filippo A. E. Nuccio]

Or are there other arguments against?

[Christian Merten]

You have to fix the name of every declaration that mentions IsLimit (and IsColimit) as well and deprecate every single one of them. I am not sure this is worth it.

[Robin Carlier]

if we are to rename it, I would prefer LimitStruct, but as Christian just beat me to it, we also have a considerable amount of docstrings/related names using this naming, so this would be one hell of a deprecation streak.

[Filippo A. E. Nuccio]

OKOK, no problem. I certainly agree it is not a major issue.