Skip to main content

All Questions

Filter by
Sorted by
Tagged with
13 votes
1 answer
933 views

Consistency strength of HoTT

What is the consistency strength of Homotopy type theory (HoTT) relative to various set theories (e.g., are there any known set theories that it can interpret)? Does this question even make sense?
Jesse Elliott's user avatar
12 votes
3 answers
649 views

Has the Ramified Theory of Types been applied to NBG?

Questions of predicativity are well-studied in the context of arithmetic. We have a base theory, first-order Peano arithmetic. Some people, like Edward Nelson (in chapter 1 of his book) and Charles ...
Keshav Srinivasan's user avatar
7 votes
2 answers
1k views

Explaining the consistency of PRA and ZF from predicative foundations

Recently I got interested in predicative foundations, mostly because of Laura Crosilla's work and because Agda employs a predicative type theory. From the point of view of a predicative foundation to ...
Ingo Blechschmidt's user avatar