Timeline for A (very naive) question about Homotopy Type Theory
Current License: CC BY-SA 3.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 8, 2013 at 8:04 | comment | added | Philippe Gaucher | This is an additional comment to my post. What is remarkable is not that there is a homotopy theory of types: after all, there are a lot of homotopy theories of many kinds of objects. What is remarkable is that the homotopy theory of logical types behaves exactly like "standard" homotopy types. And also, there are other coincidences in mathematics which are indeed not very fortunate. Some adjectives like "regular" or "normal" are semantically overloaded. | |
| Aug 7, 2013 at 17:42 | answer | added | Peter Aczel | timeline score: 8 | |
| Aug 7, 2013 at 4:34 | history | edited | François G. Dorais |
edited tags
|
|
| Aug 7, 2013 at 3:13 | comment | added | Baby Dragon | @S.Carnahan I mean that we do not get too far away from the box for physical and psychological reasons (Oddly the way we speak about boxes is squarely in the box). I should note that this idea is not completely fleshed out. | |
| Aug 7, 2013 at 2:09 | vote | accept | Philippe Gaucher | ||
| Aug 7, 2013 at 0:51 | comment | added | S. Carnahan♦ | @BabyDragon When you say "think in predic(t)able ways", do you mean in the sense that we are able to communicate meaningfully with each other without spelling everything out completely, or in the sense that we don't break out of the box much? | |
| Aug 6, 2013 at 20:53 | answer | added | Urs Schreiber | timeline score: 16 | |
| Aug 6, 2013 at 19:21 | comment | added | Baby Dragon | I am inclined to think that this is not a mere coincidence. Rather, that this is some sort of reflection of the fact that mathematicians tend to think in predicable ways. | |
| Aug 6, 2013 at 19:19 | comment | added | Andrej Bauer | It seems that HoTT is fashionable enough that the hawks have not descended on this question and branded it as "soft" and "not mathematical". | |
| Aug 6, 2013 at 19:11 | comment | added | Philippe Gaucher | @Jonathan Chiche: oui en somme, il nous faut faire la rencontre du troisième type. | |
| Aug 6, 2013 at 14:59 | comment | added | Urs Schreiber | It's a coincidence, but a very fortunate one (for a change). When people started saying "homotopy type" X they meant "the type of X" as in "what kind of space is X". When people said "type" X in logic, they meant the type of its terms, as in "what kind of thing is an $x \in X$ ". In a naive sense, these two usages of "type" are not actually the same. Luckily, as one digs deeper, it turns out by lucky coincidence that at the bottom of it indeed this is the same notion of "type" in both cases. I think its one of those trivialities that deserve to be regarded as "deep". | |
| Aug 6, 2013 at 14:54 | comment | added | Jonathan Chiche | Il faut demander au type qui a inventé le terme. | |
| Aug 6, 2013 at 14:39 | history | asked | Philippe Gaucher | CC BY-SA 3.0 |