Variants of HoTT¶
Book HoTT¶
Book HoTT is the type theory described in the HoTT book. The theory is given initially as intensional MLTT with a hierarchy of universes indexed by nonnegative numerals, and univalence as an axiom (and function extensionality as a theorem).
In addition, the HoTT book has an (intentionally) unspecified ability to obtain higher inductive types, and some examples are given:
- \(n\)-truncation,
- suspension types,
- pushouts,
- set quotients,
- the cumulative hierarchy \(V\),
- the surreal numbers \(\mathsf{No}\),
- the free Cauchy completion of the rationals \(\mathbf{R}_C\),
where the computation rules for HITs is given definitionally for points but propositionally for higher constructors.
Cubical type theory¶
See also the proof assistant section and CCHM [CCHMortberg17]. To get started understanding cubical type theory, it may be worth reading the demo code from the proof assistant.
Cubical type theory is a type theory for which univalence is a theorem. It adds an interval pretype which is used to define identity types. This interval is necessarily not a type. In practice, this means that you can talk about the type \(I\to A\) of functions from the interval to a type, but you can not talk about the interval \(I\) as a free-standing type.
Cubical type theory was implemented in the cubicaltt proof assistant
and the agda --cubical mode.
Although univalence is a theorem, the normal form is huge (megabytes), although it is argued that this is due to the proof rather than the design of cubical type theory.
Todo
there are variants of cubicaltt itself: “gothenburg” cubicaltt, computational type theory, conor mcbride’s work “cubical adventures”
Todo
NB: cubical sets != cubical TT. cubical sets is a semantics of two type theories: book hott and cubicaltt.
Todo
you have identity types, and path types, and they are computationally not the same (although they are htpy-equiv).
HoTT as a DSL¶
Dan Licata argues we should think of HoTT as a language to which we add features depending on how we plan to use it, in the same way that we write specialized programming languages for specific use-cases. For example, cubical type theory is a domain-specific language for programming with Kan cubical sets, and real-cohesive HoTT is a language for programming topological spaces. Shulman and Riehl have a language for programming \((\infty,1)\)-categories [RiehlShulman17].
In this sense, HoTT becomes a class of type theories.
HoTT as an approach to MLTT¶
Parts of HoTT can be developed in intensional MLTT, that is, without assuming univalence, function extensionality, propositional extensionality, or the existence of any HITs. For example:
- The fact that h-levels are cumulative (if \(A\) is an \(n\)-type then it is also an \((n+1)\)-type) does not require univalence.
- The groupoid laws of identity types and iterated identity types can be proved by simple path inductions.
- Some propositional truncations exist without assuming the existence of any HITs or propositional resizing, such as the type of fixed-points of any constant endomap \(f\) on \(X\).