The real numbers in homotopy type theory (CCA 2016 slides)

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

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?

Cale Gibbard

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!

Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.