Post #1948798

@jhostert The underlying mathematical objects being manipulated are (a specific variety of) cubical sets. But I can't explain much more since one of my purposes in starting this page is to force myself to (belatedly, given my PhD topic) understand the syntax and semantics of cubical type theory sufficiently well to be able to explain this… At any rate, I think that the HoTT book is still the best place to learn about the “types as spaces” interpretation; it will be much easier to understand cubical type theory if you first have a working understanding of the HoTT book (one may hope that eventually there will be introductions to cubical type theory that don't presuppose this knowledge, but that's how it is at the moment).