* table of contents {: toc} ## Overview 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](http://mathoverflow.net/questions/69229/proof-strength-of-calculus-of-inductive-constructions) on the proof theoretic strength of pCIC. Avigad provide a general overview of the proof theory of predicative constructive systems. ## References * {#Avigad} Jeremy Avigad, _Proof Theory_, 2014 [PDF](https://www.andrew.cmu.edu/user/avigad/Papers/formal_epistemology.pdf) * {#Setzer} Anton Setzer, _Proof theoretical strength of Martin-Lof Type Theory with W-type and one universe_ [PDF](http://cs-svr1.swan.ac.uk/~csetzer/articles/weor0.pdf). * {#Voevodsky} Vladimir Voevodsky, _Notes on type systems_ 2011 [PDF](http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/expressions_current.pdf). * {#Coquand} Thierry Coquand et al, _Variation on Cubical sets_, 2014 [PDF](http://www.cse.chalmers.se/~coquand/comp.pdf).