Timeline for Extensionality in HoTT versus extensionality in internal language of a category
Current License: CC BY-SA 3.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 4, 2014 at 9:13 | comment | added | Andrej Bauer | I am growing tired of this discussion. The question is not well posed because it uses the slippery concept of "extensionality". I have answered as well as I could to clear up things. You keep saying that $\mathsf{Id}$ is the extension of $\equiv$. I already explained why I disagree, so let's leave it at that. | |
| Nov 4, 2014 at 8:54 | comment | added | user40276 | @AndrejBauer Are you assuming "proposition as types" or you are restricting the values of $P$ to h-level 1 types? Furthermore in this case seeing $Id_A(x, y)$ and $x \equiv_A y$ as a type, their extensions would be the dependent sum, does this match with the definition of (definitionally) extensional type theory? | |
| Nov 3, 2014 at 21:43 | comment | added | Andrej Bauer | The extension of a predicate $P : A \to \mathsf{Type}$ is the type $\sum_{x : A} P(x)$. | |
| Nov 3, 2014 at 21:29 | history | edited | user40276 | CC BY-SA 3.0 |
deleted 6 characters in body
|
| Nov 3, 2014 at 21:29 | comment | added | user40276 | But I agree that definitional is just a characteristic of the judgmental equality, so I will change it. | |
| Nov 3, 2014 at 19:56 | comment | added | user40276 | @AndrejBauer the judgmental equality is definitional (actually computational). Furthermore it's an element of the deductive system, so it's part of the metalanguage, so it makes sense to talk about extensions. Maybe this question is quite subjective since "extension" is a philosophical concept… | |
| Nov 3, 2014 at 16:19 | comment | added | Andrej Bauer | I am not sure it makes sense to speak of the "extension of judgmental equality" (please do not call it "definitional") because judgmental equality is not a type or an element of a type, or anything like that. It is a judgment. | |
| Nov 3, 2014 at 15:49 | history | edited | user40276 | CC BY-SA 3.0 |
added 230 characters in body
|
| Nov 3, 2014 at 15:06 | history | edited | user40276 |
edited tags
|
|
| Nov 3, 2014 at 8:25 | answer | added | Andrej Bauer | timeline score: 10 | |
| Nov 3, 2014 at 7:41 | history | edited | user40276 | CC BY-SA 3.0 |
added 17 characters in body
|
| Nov 2, 2014 at 20:48 | answer | added | Mike Shulman | timeline score: 6 | |
| Nov 2, 2014 at 20:44 | history | edited | Paul Taylor | CC BY-SA 3.0 |
trimmed the suppicatory language
|
| Nov 2, 2014 at 18:47 | answer | added | Paul Taylor | timeline score: 0 | |
| Nov 2, 2014 at 13:19 | history | asked | user40276 | CC BY-SA 3.0 |