6 thoughts on “The real numbers in homotopy type theory (CCA 2016 slides)

  1. 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.

  2. @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.

  3. 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.

  4. @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!

Leave a Reply to Cale Gibbard Cancel reply

Your email address will not be published. Required fields are marked *

*