Jason (jcreed) wrote,

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
Tags: categories, talks

  • (no subject)

    K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded