Showing changes from revision #2 to #3:
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.
This section collects some references that establish the strength various type theories, roughly in increasing order of strength.
Let denote MLTT without inductive types and universes closed under and . This has the strength of the first-order system of iterated fixed points (whether with intuitionistic or classical logic), and thus by Feferman 1982 has proof-theoretic ordinal , where and .
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.