Remark on "extensionality" in notes to Chapter 2

[martinescardo]

The last sentence of the first paragraph of the Notes to Chapter 2 says: "One may argue, however, that homotopy type theory is in another sense more “extensional” than traditional extensional type theory, because of the function extensionality and univalence axioms."

This is misleading, because in extensional type theory, funext is provable. It is true that univalence can be regarded as a form of extensionality (but this is never explained in the book anyway, as far as I can see), stronger than funext. Hence this sentence should be rewritten, I think.

[andrejbauer]

In the presence of the eta-rule, I suppose?

[mikeshulman]

This sentence has another problem, namely that if I understand correctly, historically "extensional" type theory was so named not because it is more extensional than intensional type theory, but because it was less intensional, the reflection rule preventing judgmental equality from being able to represent an intensional notion of equality that is stronger than the extensional one.

[mikeshulman]

What do you think of #617 ?

[andrejbauer]

It's a good try to get things fixed. I think many people think that intensional type theory is so called because of the presence of identity types.

[vladimirias]

I suggest to have a look at notions of "intensionally equal" and "extensionally equal" in here http://en.wikipedia.org/wiki/Combinatory_logic .

V.

On Jan 20, 2014, at 3:50 PM, Andrej Bauer notifications@github.com wrote:

It's a good try to get things fixed. I think many people think that intensional type theory is so called because of the presence of identity types.

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

[mikeshulman]

Vladimir, that seems to me to be saying the same thing?

[DanGrayson]

I like the proposed pull request, and would suggest changing onlythe "extensional'' identity type to an "extensional'' identity type, as identity types acquire extensional features only when axioms are added.

[mikeshulman]

Hmm, the extensionality features of funext and UA are only imposed by axioms (at least, in type theories currently in use), but I think even without those axioms, identity types (in intensional type theory) are more extensional than judgmental equality is. For instance, we have n+m=m+n for all n,m:N, which is not true judgmentally.

[DanGrayson]

Good point. I wasn't thinking of that as an aspect of extensionality, but it is, so I retract my suggestion. (If find these adjectives tricky, so it's good to think about them.)

On Wed, Jan 22, 2014 at 2:11 PM, Mike Shulman notifications@github.comwrote:

Hmm, the extensionality features of funext and UA are only imposed by axioms (at least, in type theories currently in use), but I think even without those axioms, identity types (in intensional type theory) are more extensional than judgmental equality is. For instance, we have n+m=m+n for all n,m:N, which is not true judgmentally.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/600#issuecomment-33056283 .