Showing changes from revision #1 to #2:
Added | Removed | Changed
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.
The universe 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 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 , since by contractibility of , any two “fibrantly-replaced” types would be equal. However, it may be possible to allow fibrant replacement of specific types in the empty context.
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 samemodel invariance problem -topos can may have fail: different distinct “internal model languages” categories according presenting to the HTS. same-topos might have different “internal languages” according to HTS. This is probably the case if we allow fibrant replacements; it is less clear otherwise.
Revision on March 11, 2014 at 06:46:49 by Mike Shulman. See the history of this page for a list of all contributions to it.