Discrete differential geometry in homotopy type theory

A homemade version of my masters thesis defense talk at Carnegie Mellon University in April, 2025.

The full thesis: https://arxiv.org/abs/2504.20363
PDF of slides at: https://greg.langmead.info/writing/differential_geometry_in_hott

If you are new to homotopy type theory, a good starting point is Dan Christensen’s talk here: https://www.youtube.com/watch?v=_0sEEAMwHzo

00:00 Intro
00:35 Gauss-Bonnet and Poincaré-Hopf
04:14 HoTT prerequisites
04:38 Combinatorial manifolds
17:06 Torsors
22:29 Connections and curvature
34:41 Vector fields
52:16 Main theorem

Видео Discrete differential geometry in homotopy type theory канала Greg Langmead