chore(category_theory/limits): unify naming of lemmas related to the (co)lim functor

[TwoFX]

lim.map_π was the only lemma of the form lim.* rather than limit.*, and I do not see any way it differs from limit.map_pre and others that could justify the different naming.

[jcommelin]

I think the reason it was called lim.map_pi is that the statement starts with lim.map \alpha .... Hence it follows the naming conventions, and I'm inclined to leave it the way it was...

[TwoFX]

This makes sense, but I feel that if the name lim.map_pi is used, then the name lim.map_pre should also be used instead of limit.map_pre. On the other hand, limit.map_pre' would still be correct, so a series of very closely related lemmas would have different prefixes.

As someone who tried to use these lemmas, I found the current situation to be very confusing, and I chose this way of unification because it looked like it would require the fewest changes, but I'd be happy to change the PR to instead rename limit.map_pre (and maybe limit.map_post?).

[jcommelin]

@TwoFX Fair enough, I agree with the confusion. I think that limit.map_pre is actually the one that is "violating" the naming convention. If you want to PR those changes, that would be nice.

[TwoFX]

@jcommelin I have adapted the names of the lemmas as discussed. Note that in this version the naming is not consistent across duals. For example, we have lim.map_π, but its dual is called colimit.ι_map. (I am not trying to say that this is a bad thing. I just want to draw attention to it in case it is.)

[jcommelin]

Hmmm... I agree that that is also confusing. I think being consistent across duals is maybe more important than other considerations. @semorrison do you have some helpful advice?

[semorrison]

Let's just name everything with limit. or colimit.. I think uniformity is better than any of the non-uniform rules, all of which have some surprise factor.

(The underlying confusion here is that I decided to use the shortened lim and colim for the "limits packaged as a functor" gadgets. Another alternative would be to work out if we can rename those.)

So --- @TwoFX, would you mind restoring your PR to the original state?

[TwoFX]

So --- @TwoFX, would you mind restoring your PR to the original state?

Done.

[jcommelin]

Cool, I agree with Scott, after second thought. It's on the merge queue.