Here are materials related to Vladimir's proposal for a type theory with two kinds of equality, called Homotopy Type System (HTS).
  • Notes on HTS.
  • Slides from a talk given on Joyal's 70th birthday, 2/25/13.

Note: this is work in progress.