In reply to
Carlo Angiuli
@carloangiuli@mathstodon.xyz
Assistant Professor in Computer Science at Indiana University. Into (homotopy) type theory & programming languages.
mathstodon.xyz
Carlo Angiuli
@carloangiuli@mathstodon.xyz
Assistant Professor in Computer Science at Indiana University. Into (homotopy) type theory & programming languages.
mathstodon.xyz
@carloangiuli@mathstodon.xyz
·
Mar 06, 2026
@ryanbrewer There's a video here at https://hott-uf.github.io/2020/ but a ton has changed and I would disrecommend watching the talk to learn about gluing. (Maybe the first half, which includes these slides, is still worth watching.)
One resource for both topics is the book on dependent type theory I'm writing with @danielgratzer, although unfortunately cubical type theory + gluing are like......the two unfinished parts of the book, lol. But here's the draft: https://carloangiuli.com/papers/type-theory-book.pdf (updated public draft coming soon!)
View full thread on mathstodon.xyz
3
2
1
Conversation (2)
Showing 0 of 2 cached locally.
Syncing comments from the remote thread. 2 more replies are still loading.
Loading comments...