[gallabytes]

A lot of work was going into the cubical model, but IIRC they realized it was a dead end about a month and a half ago. Right now the most promising work looks to be formalizing the set theoretic model in NuPRL.

[Kutta]

Could you give pointers wrt cubical model being a dead end? As yet I've heard nothing about this.

[doall]

See this https://groups.google.com/d/msg/homotopytypetheory/oXQe5u_Mm...