Adjustments to pointed spaces

pType is now Set*, to make the notation more uniform, and we're using
sigma instead of a homebrew dependent product (in particular, no
overloading of the _,_ constructor; it's the same thing now).
Extra pointed space functions.

Identity function; constant functions.