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

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

Remarks

• The universe $U$ of non-fibrant types is itself fibrant. In the simplicial set model of HTS, and in many other categorical models, this universe is itself contractible (in the usual sense of homotopy type theory, with respect to the $Paths$ identity type). It is unclear whether it can be proven to be contractible inside HTS.

• It is impossible to add a generic “fibrant replacement” type former $R:U\to U_F$, since by contractibility of $U$, any two “fibrantly-replaced” types would be equal. However, it may be possible to allow fibrant replacement of specific types in the empty context.

• Mike Shulman has argued that rather than assuming the natural numbers type to be fibrant and yet able to eliminate into non-fibrant types, there should be two natural numbers types: a fibrant one which can only eliminate into fibrant types, and a non-fibrant one which can eliminate into all types. This is because while the natural numbers type in simplicial sets happens to be fibrant, that is not the case in other categorical models, and it may pose similar problems for constructing new models of HTS out of old ones.

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 model invariance problem may fail: distinct model categories presenting the same $(\infty,1)$-topos might have different “internal languages” according to HTS. This is probably the case if we allow fibrant replacements; it is less clear otherwise.