Documentation for universe polymorphism

By `Show` I meant `About` (there is no `Show foo` command).  `Check` also prints universe constraints, but it gives a possibly different list, possibly collapsing some of them.  I guess this is because it treats its argument as a term to be typechecked rather than a definition to be described.  I'll add a comment about this.