Homotopy Type Theory Homotopy Type System > history (Rev #1)

Proposed by Vladimir Voevodsky, Homotopy Type System (HTS) is a type theory with two equality types, an “exact” or “strict” one which satisfies a reflection rule?, and a “path” or “homotopical” one which does not. It also distinguishes between “fibrant” and “non-fibrant” types: the path type only eliminates into fibrant types.

Specification

• Homotopy Type System

Implementation

• In progress: https://github.com/andrejbauer/tt

Pros

• HTS should allow a definition of semisimplicial types and other infinite objects, by requiring diagrams of types to commute strictly using the exact equality.

Cons

• In the specification as written above, inductive types are fibrant as long as all their inputs are, but this is not the case in all desired models.

• The system is not homotopy invariant at the level of models: distinct model categories presenting the same $(\infty,1)$-topos can have different “internal languages” according to HTS.