Push ID - Merge Imminent

This is Martin's Push ID PR split off from unidirectional.  Given that it has already been picked over in those contexts and the feedback from that and in-person discussion was to bring this change in separately, I'm about ready to merge this.  Everything anyone has quibbled with has been editorial.  However, I don't see reviews from many folks, so I want to make sure that everyone interested has had a chance to express an opinion.

https://github.com/quicwg/base-drafts/pull/701

I'll give it a few hours (until everyone's had at least a little bit of a work day), then merge unless I hear otherwise.