Impredicativity of hProp

[mikeshulman]

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]

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//issues/8
.

[vladimirias]

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//issues/8
.

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

[andrejbauer]

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.