# Type Theory and Differential Geometry

For people who’ve known me long, you’ll have heard at least a dozen times that differential geometry was, in fact, my first love. When I was a freshman in undergrad, I discovered a copy of Baez and Muniain’s “Gauge Fields, Knots, and Gravity”. This book was my first introduction to both differential geometry and its applications in understanding physics. I was pretty much hooked after this and I took a couple of graduate courses on the topic, read a bunch of books, did some research with a postdoc, and while I eventually moved into experimental I still have a lot of my old books: including a copy of Jost’s Riemannian Geometry and Geometric Analysis that I never actually finished because I was getting my master’s in physics shortly after picking it up.

In any case, I loved geometry. Over the last few years, I’ve moved more and more into foundational mathematics and logic but I’ve had ideas about geometry in the back of my head for awhile. In particular, I’ve wondered off and on about how to actually encode the basics of geometry in type theory. I never thought that hard about it until I saw this post by Wren Thornton about describing the type of derivatives and I thought it was really cute the way you could describe different notions of derivative over reals as just one family of types.

So what happens if, say, we want to encode the idea of atlases, one of the basic things one needs to define differentiable manifolds? Well, first let’s review what an atlas is. An atlas is a collection of charts, where a chart is a pair of an open set $U_{\alpha}$ in the topological space and a function $f_{\alpha} : U_{\alpha} \to \mathbb{R}^n$ such that there is an open set of $\mathbb{R}^n$ that is the homeomorphic image of $U_{\alpha}$. To encode this in type theory, we’re obviously going to need a way to describe a notion of isomorphisms. Now, whenever we’re talking about isomorphisms my brain immediately goes to higher dimensional type theories. Whenever we’re talking about applications of higher-dimensional type theories in mathematics I either start looking at http://ncatlab.org or http://homotopytypetheory.org/. Well, I found this which appears to be a work in progress(?) which seems like it’s redoing a lot of the math I learned years ago in a more formal type-theoretic way. This is something I’ll probably be reading off and on in the near future, because on some level mathematical physics is something I’ll always love.

I think I’ll also probably pull out some of my old books in order to relearn some of the geometry I’ve forgotten. Maybe it’s silly, but I’m really excited by the prospect of returning to my first academic loves but with the tools of foundational mathematics I’ve learned since I was a kid eating up every math book I could find.