Thomas Streicher (Darmstadt)


Identity Types vs. Weak \omega-Groupoids some ideas, some problems

ABSTRACT After reviewing some basics about Identity Types in intensional
         Martin-Löf type theory and shortly presenting the groupoid model
         I explain why every type forms an internal weak \omega-groupoid.
         It thus seems tempting to use Kan complexes as a model. But there
         are problems with the Beck condition. I sketch an idea how to define
         a sufficiently internal notion of Kan complexes allowing to choose
         "fillers" in a functorial way. This notion might be of interest for
         geometers as well.
         Finally, I discuss to which extent a weak \omega-groupoid model
         says something about the types definable in traditional type theory.
         I am afraid nothing because their interpretations all stay within 
         discrete simplicial sets.