More replacement of [projT] with [pr]

The instances of [proj1_sig] in Category/Sigma are intentional and semantically meaningful (they are about subsets/sigT with an hProp).  This builds on #437.