Post #1763206

2026-04-24 15:58 UTC

I just created a Wikipedia page about cubical type theory. For now this is a stub with just keyword-dropping and reference-dropping. Help to augment it is very welcome, we really need a readable first introduction to cubical type theory written down somewhere. https://en.wikipedia.org/wiki/Cubical_type_theory

Replies (1)

@jhostert@mathstodon.xyz 2026-04-25 22:23

@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 💪

Open ##1948796