Timeline for Extensionality in HoTT versus extensionality in internal language of a category
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 3, 2014 at 7:33 | comment | added | user40276 | Thanks for the answer, but I already knew everything you have said. My point is different (and I have a background in category theory), I know what $x=_A y$ means (the proofs or evidences of the equality, i.e., an internalization of a judgment). I want to know what is the extension of a predicate in HoTT. "Extension" is a concept of mathematical philosophy and in the case of classical logic (I don't know the intuitionistic case, maybe this would be the answer the my question) it's considered to be the collection of elements (terms in the context of type theory) that satisfies the predicate. | |
| Nov 2, 2014 at 20:48 | comment | added | Steven Gubkin | I think the first sentence of your post is not very helpful. Of course, that is just an opinion. I do not think I will comment further. | |
| Nov 2, 2014 at 20:41 | history | edited | Paul Taylor | CC BY-SA 3.0 |
added 250 characters in body
|
| Nov 2, 2014 at 20:35 | comment | added | Paul Taylor | My post was written exactly to be diplomatic, and tutorial, with a view to encouraging the questioner to pursue the study of this topic. Unfortunately, the same cannot be said of most of the responses to naive questions from students that appear on this site: similarly phrased questions on slightly different topics are peremptorily closed. | |
| Nov 2, 2014 at 20:30 | history | edited | Paul Taylor | CC BY-SA 3.0 |
added 381 characters in body
|
| Nov 2, 2014 at 19:13 | comment | added | Steven Gubkin | You might consider editing this post to be a bit more diplomatic? | |
| Nov 2, 2014 at 18:47 | history | answered | Paul Taylor | CC BY-SA 3.0 |