What always makes me itch about this business is that it comes out very naturally as an ω-groupoid, because you're talking about equality after all, and not more generally an ω-category. I suppose you'd want to suppose an abstract asymmetric relation in your type theory, but heck if I know how you'd want to interpret it. Which is to say, I guess: heck if I know what its elimination rule should be, either.
Two other things of note that came up during and just after the talk:
(1) Rick Statman interrupted when Peter was explaining what it meant to be a well-formed context in the setting of dependent types, and asked why contexts had to be ordered and acyclic. Aha! I thought, maybe people have totally worked out how that makes sense, and I don't have to invent it all from scratch to get typing of metavariable contexts in LF unification working after all. But no, apparently it's merely something that's been "in the air" from time to time, and it has never gotten used as far as Statman let on.
(2) Noam explained more about his alternative-HOAS-y idea to me, to the point that I have an overwhelming suspicion that it's good for something, but I can't see precisely what