September 30th, 2008

beartato phd

(no subject)

Peter Lumsdaine gave a seminar talk setting up some framework to talk about the relationship between intensional Martin-Löf type theory and weak ω-groupoids in the next couple weeks. Somehow I never feel totally confident working my way around old Martin-Löf-ish style stuff. Something about treating definitional equality so much in terms of reduction rules rather than canonicalization. At least he's not going to do something so horrifically promiscuous as the extensional version, where Id-types go right ahead and infect definitional equality.

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