The real numbers in homotopy type theory (CCA 2016 slides)
- 15 June 2016
- Type theory, Talks
I am about to give an invited talk at the Computability and Complexity in Analysis 2016 conference (yes, I am in the south of Portugal, surrounded by loud English tourists, but we are working here, in a basement no less). Here are the slides, with extensive speaker notes, comment and questions are welcome.
Slides: hott-reals-cca2016.pdf
How to comment on this blog:
At present comments are disabled because the relevant script died.
If you comment on this post on Mastodon and
mention
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
Is there a link or a citation to the higher inductive-inductive presentation of the Sierpinski space that you mentioned on the last slide? I had not heard of that before.
@Andrej: The slides look nice. I wonder how people react to: "realizability models (and thus TTE)." :-) Maybe be a little less assertive that the Dedekind reals are not possible too in HoTT?
@Mike: http://www.cse.chalmers.se/~nad/publications/altenkirch-danielsson-types2016.pdf http://www.cse.chalmers.se/~nad/listings/partiality-monad/README.html We also speculated a bit about this direction at the IAS. e.g. 11.2.(iv) in the book. However, we didn't pursue it at that time.
I'm quite curious about what the higher homotopy is that we're killing off when we do the truncation. Certainly if we're aiming to define the set of real numbers, we should have such a truncation, but it feels a bit hasty, we might be throwing away something interesting about real numbers which could not be observed by classical means. (We also might not, it might be boring, but I'd like to know!)
If we leave out the truncation, we can consider the type Id R u u, and we can ask questions about whether Id R u u = Id R v v for a given pair of untruncated reals u and v. Will we always find such an equivalence, or does it reveal something number theoretical about u and v? Given the construction, it certainly wouldn't be too surprising to find that rationals have different local path structures than limit points...
This is just an itch that's been at the back of my mind since reading the HoTT book, I haven't really begun to approach it in a serious way. I'm curious if anyone else has had the same thought and more time to think about it.
Andrej, thanks for sharing the slides! Mike: Andrej is referring to the "Partiality monad" as a HIT, see here: abstract and slides. For the unit type (i.e. 1-bot), this gives the Sierpinski space.
I was also interested in the Sierpinski space construction he mentioned, and I found it on the TYPES website here: http://www.types2016.uns.ac.rs/images/abstracts/altenkirch2.pdf
@Cale: If we leave out the set truncation then we will get the freely generated higher-path structure, whatever that is, because we have an inductive definition. I have not thought whether this structure could be interesting, I always presumed it is not. But who knows!