Homotopy Type Theory
proof theoretic strength of univalent type theory plus HITs


This is a stub collecting information on the question in the title. 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.

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 ML n\mathrm{ML}_n denote MLTT without inductive types and nn universes closed under Π\Pi and Σ\Sigma. This has the strength of the first-order system of nn iterated fixed points (whether with intuitionistic or classical logic), and thus by Feferman 1982 has proof-theoretic ordinal ξ n\xi_n, where ξ 0=ε 0\xi_0=\varepsilon_0 and ξ n+1=φ(ξ n,0)\xi_{n+1} = \varphi(\xi_n,0).