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

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 on the proof theoretic strength of pCIC. Avigad provide a general overview of the proof theory of predicative constructive systems.

References

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