Timeline for Do higher types in HoTT provide mathematical structures beyond ZFC?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 25 at 12:59 | comment | added | Timothy Chow | @AlecRhea See for example Mariano Carneiro's master's thesis (it deals with Lean and not HoTT, but I think it is still pertinent). Roughly speaking, it shows that Lean is "equivalent" to ZFC + infinitely many inaccessibles. | |
| Jul 25 at 12:57 | comment | added | Timothy Chow | I find the following analogy helpful: Comparing HoTT and ZFC is akin to comparing two different programming languages. In any sufficiently powerful programming language, you can do anything that you can do in any other language. Nevertheless, different programming languages have different merits. Some goals are easier to achieve in one language than another, and some kinds of bugs are more likely to occur in one language than another. So "redundancy" and "uniqueness" are in some sense beside the point. | |
| Jul 24 at 16:08 | comment | added | Corbin | On (2), it's always worth considering the constraints of the underlying logical framework; ZFC is first-order, and there are several classes of structures which aren't first-order-izable. The "necessity and utility of these higher types" is not specific to HoTT. | |
| Jul 23 at 21:23 | history | became hot network question | |||
| Jul 23 at 21:21 | vote | accept | Pan Mrož | ||
| Jul 23 at 21:24 | |||||
| Jul 23 at 21:09 | history | edited | YCor | CC BY-SA 4.0 |
formatting
|
| Jul 23 at 21:04 | answer | added | Andrej Bauer | timeline score: 8 | |
| Jul 23 at 15:10 | comment | added | Alec Rhea | As someone almost completely ignorant of type theory, my understanding is that we have an array of equiconsistency/interpretability results between set theories and type theories which imply that anything one can do, the other can do better. (mama mia!) But I would be interested to hear from someone less ignorant. | |
| Jul 23 at 12:57 | history | asked | Pan Mrož | CC BY-SA 4.0 |