Improve the discussions on TemplatePoly and UnivPoly

[thomas-lamiaux]

Improve the discussions on TemplatePoly and UnivPoly, in particular on performances
https://github.com/coq/platform-docs/blob/main/src/Explanation_Template_Polymorphism.v

[MevenBertrand]

I have a few minor improvements (basically, typos, including one in the code), for now it's on a branch of mine here. I can open a PR if you want them.

The tutorial makes it sound like universe poly is strictly better than template poly in most (all?) cases. However, there is the caveat that template poly also extends to Prop and Set (and SProp, too, I think), but universe poly does not: you cannot replace a polymorphic universe by Prop. This is somewhat implicit in the tutorial, but might be better to make explicitly?

Also, this is the reason for the new and shiny sort polymorphism coming up starting in 8.19 (not sure this is worth mentioning at this point, but that means that the tutorial might need changes once sort poly is consolidated).

[SkySkimmer]

univ poly handles Set and sort poly handles Prop/SProp
template poly does not handle SProp

[MevenBertrand]

I thought there were (used to be?) restrictions about replacing a universe poly variable with Set, but my bad!

[thomas-lamiaux]

Don't hesitate to make a PR if you have improvements.
The tuto is a bit biased hence this issue, and we hope to improve over time with contributions