nLab proof theoretic strength of univalent type theory plus HITs

Overview

This is a stub collecting information on the proof theoretic strength of univalent type theory with higher inductive types.

Setzer computes the strength of MLTT+W. Voevodsky reduces Coq’s inductive types to W-types. Coquand et al reduces univalence and some HITs to an unspecified constructive framework, which can be taken to be CZF+REA with a sequence of universes. It follows from this work that univalent type theory and these HITs has the same proof theoretic strength as MLTT with inductive definitions and a sequence of universes.

There is an MO-question on the proof theoretic strength of pCIC. Avigad provide a general overview of the proof theory of predicative constructive systems.

The strength of type theories

This section collects some references that establish the strength various type theories, roughly in increasing order of strength.

Let $\mathrm{ML}_n$ denote MLTT without inductive types and $n$ universes closed under $\Pi$ and $\Sigma$. This has the strength of the first-order system of $n$ iterated fixed points (whether with intuitionistic or classical logic), and thus by Feferman 1982 has proof-theoretic ordinal $\xi_n$, where $\xi_0=\varepsilon_0$ and $\xi_{n+1} = \varphi(\xi_n,0)$.

References

• Jeremy Avigad, Proof Theory, 2014 PDF

• Thierry Coquand et al, Variation on Cubical sets, 2014 PDF.

• Solomon Feferman, Iterated inductive fixed-point theories: application to Hancock’s conjecture, Stud. Logic Foundations Math., 109, 1982.

• Anton Setzer, Proof theoretical strength of Martin-Lof Type Theory with W-type and one universe PDF.

• Anton Setzer, Proof theory of Martin-Löf type theory. An overview PDF

• Vladimir Voevodsky, Notes on type systems 2011 PDF.