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

Showing changes from revision #0 to #1: 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.


  • Jeremy Avigad, Proof Theory, 2014 PDF

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

  • Vladimir Voevodsky, Notes on type systems 2011 PDF.

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

Revision on January 12, 2015 at 19:27:53 by Bas Spitters. See the history of this page for a list of all contributions to it.