search

HoTT / book

A textbook on informal homotopy type theory
2.01k stars 358 forks source link

Impredicativity of hProp #8

Closed mikeshulman closed 11 years ago

mikeshulman commented 11 years ago

The axiom of impredicativity of hProp needs to be discussed somewhere, probably in 2.8. I think chapter 9 implicitly assumes this, but is it used anywhere else?

spitters commented 11 years ago

What is currently the best source for the resizing rules: http://uf-ias-2012.wikispaces.com/file/view/Universe+polymorphic+type+sytem.pdf or perhaps http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_Bergen.pdf

Bas

On Fri, Mar 8, 2013 at 1:27 PM, Mike Shulman notifications@github.comwrote:

The axiom of impredicativity of hProp needs to be discussed somewhere, probably in 2.8. I think chapter 9 implicitly assumes this, but is it used anywhere else?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/8 .

vladimirias commented 11 years ago

Probably also the slides for my talk at Joyal's conference (HTS_slides.pdf in the wiki). V.

On Mar 8, 2013, at 2:40 PM, spitters wrote:

What is currently the best source for the resizing rules: http://uf-ias-2012.wikispaces.com/file/view/Universe+polymorphic+type+sytem.pdf or perhaps http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_Bergen.pdf

Bas

On Fri, Mar 8, 2013 at 1:27 PM, Mike Shulman notifications@github.comwrote:

The axiom of impredicativity of hProp needs to be discussed somewhere, probably in 2.8. I think chapter 9 implicitly assumes this, but is it used anywhere else?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/8 .

— Reply to this email directly or view it on GitHub.

andrejbauer commented 11 years ago

Thorsten pointed out to me over tea that excluded middle for hprop implies impredicativity (because hprop becomes "equivalent" to bool). We should presumably mention this, too.