Timeline for Major applications of the internal language of toposes
Current License: CC BY-SA 4.0
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 9, 2022 at 14:06 | comment | added | Bas Spitters | Applications in functional analysis: Banach algebras and C*-algebras | |
| Jan 9, 2022 at 14:05 | comment | added | Bas Spitters | There is also our work on probabilistic programming: synthetically and using realizabiltity. There is the work on the topos of trees and it's application to guarded cubical type theory. | |
| Jan 9, 2022 at 14:01 | comment | added | Bas Spitters | Other applications include nominal sets, applications to multivariate complex analysis, and cubical type theory. For the latter: Orton Pitts and LOPS. The ideas go back to a short note by Thierry Coquand. | |
| Jan 9, 2022 at 13:57 | comment | added | Bas Spitters | The work on Bohr toposes may be relevant to what you are looking for. | |
| Dec 27, 2021 at 12:37 | comment | added | Zhen Lin | @MikeShulman I recently learned (on Zulip, as it turns out) there is a recent thesis that tries to work out for internal set theory what elementary toposes do for ordinary set theory. | |
| Dec 26, 2021 at 17:11 | comment | added | Mike Shulman | @wlad I think that would be a good answer if you include a link or some explanation of how NSA can be regarded as the internal language of a topos. (Presumably you're thinking of the filterquotient topos by a nonprincipal ultrafilter.) | |
| Dec 26, 2021 at 16:41 | history | became hot network question | |||
| Dec 26, 2021 at 15:29 | answer | added | Zhen Lin | timeline score: 17 | |
| Dec 25, 2021 at 22:45 | comment | added | wlad | "Abraham Robinson and Allen Bernstein used nonstandard analysis to prove that every polynomially compact linear operator on a Hilbert space has an invariant subspace." | |
| Dec 25, 2021 at 22:43 | comment | added | wlad | I'm wondering if Non-Standard Analysis counts as a "baby example". Some breakthrough analysis results, including by Abraham Robinson himself, make use of it. | |
| Dec 25, 2021 at 22:33 | comment | added | Erik Walsberg | I don't actually know much about it but the work of Ingo Blechschmidt looks interesting, arxiv.org/abs/2111.03685 | |
| Dec 25, 2021 at 22:28 | history | edited | Stefan Kohl♦ |
edited tags
|
|
| Dec 25, 2021 at 22:28 | history | made wiki | Post Made Community Wiki by Stefan Kohl♦ | ||
| Dec 25, 2021 at 20:32 | answer | added | Paul Taylor | timeline score: 7 | |
| Dec 25, 2021 at 18:55 | history | asked | user1005113 | CC BY-SA 4.0 |