Homotopy Type Theory
proof theoretic strength of univalent type theory plus HITs (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


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


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

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

Revision on January 15, 2015 at 20:44:12 by Ulrik Buchholtz. See the history of this page for a list of all contributions to it.