Talk - The Univalence Axiom

01 Dec 2021 - Tags: my-talks

Today I gave my first proper invited talk, which was really exciting! I spoke at CMU after I graduated, but I knew the organizers so it didn’t really feel like an invitation. Jake Park at the University of Florida, though, invited me to give a talk about HoTT type theory in their department. I was and am super grateful for the opportunity, and I think the talk itself turned out fairly well too!

I wasn’t sure what kind of background to expect, so I wanted to make sure the talk was fairly beginner friendly. This was also convenient because it kept me in waters that I feel comfortable talking about. Jake requested I talk about what HoTT (particularly univalence) is used for, so I tried to emphasize what is (to me) the salient aspect of the theory: Namely the constant interplay between the logical and the geometric interpretations of the operations¹.

We started with a “quick” review of dependent types, and their dual life as propositions with a free variable and covering spaces. Then $\mathrm{\Pi }$ and $\mathrm{\Sigma }$ types are (proof relevant) universal and existential quantifiers (respectively) or global sections and the total space (respectively).

Next up was identity types (or path types), which logically correspond to propositions of the form $a\stackrel{?}{=}b$, and geometrically correspond to the space of paths from $a$ to $b$. Considering paths between paths, paths between (paths between paths), and so on, leads us naturally to the $\mathrm{\infty }$-groupoid structure on a type $A$. I first really understood this after watching a (characteristically excellent) talk of Emily Riehl here², which I’m sure will help other people too ^_^.

Then, in order to talk about univalence, we need to talk about equivalences, so we spent some time going over equivalences and why we care, culminating in the univalence axiom:

In fact, we know slightly more than that: We know what the equivalence is, as well as the computational content associated to it. If $e:A\simeq B$, then $\mathtt{ua}(e)$ is a path from $A$ to $B$, and transporting along that path just applies $e$!

We first talked about some logical applications of univalence. For instance, if $G$ and $H$ are isomorphic as groups, then they must agree on all properties! Because they’re actually equal! There was a really great question here about some “group theoretic” properties that can distinguish isomorphic groups. For instance, two isomorphic groups acting on different objects.

The way we resolve this is by noticing that, to talk about these “bonus properties”, we need to fix some bonus data about $G$. Maybe it’s the data of a group homomorphism into a symmetric group, or into a general linear group, etc. but whatever it is, we need this extra data in order to express the question. So if we look at, say $(G,X,\alpha )$ and $(G,Y,\beta )$ as objects in the type of “groups equipped with an action³”

$$\sum _{G:\text{Group}}\sum _{X:\text{Set}}\sum _{\alpha :G\times X\to X}\text{isGroupAction(}\alpha \text{)}$$

we’ll find that even if $G$ and $H$ are equivalent, $(G,X,\alpha )$ and $(H,Y,\beta )$ might not be!

Next we wanted to talk about geometric applications of univalence, but to do that we needed to spend more time building up geometric types. So we had a brief diversion into the world of HITs (Higher Inductive Types), before using univalence to construct some covering spaces of the circle $S^1$. I ended with some resources that people might be interested in, including

• this talk of André Joyal on HoTT as foundations⁴, as well as everything from this workshop.
• I’ve already linked some of Emily Riehl’s talks on HoTT as applied to Homotopy Theory, but I’ll also shamelessly plug some work of Wes Caldwell, which you can read about here, and you can even implement Eilenberg-Maclane Spaces in HoTT! See here
• There’s a lot of great work going on in trying to actually compute with HoTT efficiently. You can hear Dan Licata talk about it here, or read about some developments on Andrej Bauer’s blog here.

---

After the talk someone asked a question about differential equations, in particular about the Lotka-Volterra Equations. It sounded like they wanted a specific theorem to do with these equations, but I never quite understood what they were looking for. I’ll assume they wanted a proof that these equations are always solvable.

The question, then, is what does a proof of solvability do when we run it as code? And the answer, perhaps unsurprisingly, is that it solves the equations!

So if you have a proof (in LEAN, say) that

$$\begin{array}{rl}\mathrm{\forall }\alpha ,\beta ,\gamma ,\delta & :{\mathbb{R}}_{>0}.\\ \mathrm{\forall }{x}_0,y_0& :{\mathbb{R}}_{>0}.\\ \mathrm{\exists }x,y& :{\mathbb{R}}_{>0}\to {\mathbb{R}}_{>0}.\\ x(0)=x_0\wedge \frac{dx}{dt}=\alpha x-\beta xy& \wedge y(0)=y_0\wedge \frac{dy}{dt}=\delta xy-\gamma y\end{array}$$

the proof would be a piece of code that takes as input positive constants $\alpha ,\beta ,\gamma ,\delta ,x_0,y_0$, and gives as output two positive functions $x$ and $y$, plus proofs that they satisfy the desired differential equations and initial conditions.

In general, if you have a theorem that says “a solution to an equation of a certain form exists”, then the proof of that theorem should tell you how to find the solution! So running the proof as code actually does find it!

The person who asked this question wanted to see actual code, so here is one option:

It does seem like most of the people pushing for formalization are algebraists and logicians. This is not a limitation of the method, though! We need more people who know things about differential equations, etc. to contribute code to these projects, and flesh out the analytic parts of the standard libraries. I’m sure there are plenty of easy theorems whose proofs could be formalized if someone who knew how to do it were willing to put the time in. Anyways – I’ll get off my soapbox now :P.

---

I actually never sent Jake a talk title or an abstract… So I don’t have one to put here, haha. But I do have slides here. The talk was also recorded, and I asked for a copy, so as soon as I have it I’ll post a link here ^_^.

---