Post #1948796

2026-04-25 22:23 UTC

@jeanas I know type theory but nothing about cubical. I'd wager the article could use some pointers to the mathematical "underlying" objects one is manipulating? Like, I tried cubical Agda and did some equality casts that I could do syntactically because it's just type theory; but the tutorial kept mentioning fancy words and saying I constructed some topological transform(ation)s (?) or something and it just went right past me. Is there some Wikipedia-ready summary of what is an interval, and how they are used to prove e.g. FunExt? Anyways that's what I'd hope to learn from the article, do with that what you will. I look forward to reading a competed article some time in the future 💪

Replies (1)

@jeanas@mathstodon.xyz 2026-04-25 22:42

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

Open ##1948798