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 * [[HTS.pdf:file]] ## 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. ## 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. [[!redirects HTS]]