Uniqueness

- Introduced a new macro `\uniq`. 
- Removed the macros `\un` and `\uppt`.
- Replaced all the instances of `\un` and `\uppt` in the text with the appropriate versions of `\uniq`.
- Called the uniqueness principle for dependent pair types by its name.
- Listed the new notation in the list of symbols.

The old notation did not appear in the list of symbols, so I left it that way.