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> ## 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.