# 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

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

## The strength of type theories

This section collects some references that establish the strength various type theories, roughly in increasing order of strength.

Let $\mathrm{ML}_n$ denote MLTT without inductive types and $n$ universes closed under $\Pi$ and $\Sigma$. This has the strength of the first-order system of $n$ iterated fixed points (whether with intuitionistic or classical logic), and thus by Feferman 1982 has proof-theoretic ordinal $\xi_n$, where $\xi_0=\varepsilon_0$ and $\xi_{n+1} = \varphi(\xi_n,0)$.

## References

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