Talk - Where Are The Open Sets?

06 Oct 2022 - Tags: my-talks

I was invited to give a talk at HoTTEST 2022, and was more than happy to accept! Ever since I was first learning HoTT I was curious how we could be sure that theorems in HoTT give us corresponding theorems in “classical” homotopy theory. Earlier this summer I spent a lot of time wrestling wtih $\infty$-categories (culminating in a series of blog posts) and I realized I was quite close to finally understanding the connection between HoTT and classical topology. I think this is a question that should have a more accessible answer (the machinery is fairly intense, but that shouldn’t prevent a high level overview) and I’m happy I was able to help fill this gap!

All in all, I think the talk went quite well! I think I did a good job making the broad ideas involved in the semantics accessible to an audience without much background, though my actual delivery was a bit jittery – I had to wake up at 7.30 to give the talk and I was basically being held up by willpower and caffeine, haha.

Now that I’ve napped, let’s write up a quick summary of the talk ^_^

---

The basic idea is to interpret the syntax of HoTT in the model category of simplicial sets $s\mathsf{Set}$. This means that anything we do in HoTT externalizes to a statement about $s\mathsf{Set}$. Then we use the quillen equivalence of $s\mathsf{Set}$ with $\mathsf{Top}$¹ in order to transfer our statement in $s\mathsf{Set}$ to a statement about $\mathsf{Top}$ (up to homotopy).

First, I spent some time discussing (very roughly) what a model structure on a category is. As a reference for a less rough idea, I mentioned a famous paper Homotopy Theories and Model Categories by Dwyer and Spalinski. Next, I gave some intuition for what a simplicial set might be, and outlined how they combinatorially encode topological spaces. For more detailed references I mentioned Friedman’s An Elementary Illustrated Introduction to Simplicial Sets as well as Singh’s thesis A Survey of Simplicial Sets.

Then came a discussion of the functors converting back and forth between $s\mathsf{Set}$ and $\mathsf{Top}$:

• geometric realization, $\lvert \cdot \rvert : s\mathsf{Set} \to \mathsf{Top}$
• singular chains, $\text{Sing}(\cdot) : \mathsf{Top} \to s\mathsf{Set}$

these form an adjunction ($\lvert \cdot \rvert \ \dashv \ \text{Sing}(\cdot)$) which respects the model structure on both categories in the sense that they form a quillen equivalence:

The punchline is that any question² we have about the homotopy theory of topological spaces can be answered by transporting to $s\mathsf{Set}$ and answering the question there³!

This is great news for two reasons:

• Concretely, simplicial sets are combinatorial, so we can describe many interesting simplicial sets to a computer with only a finite amount of data. This is the backbone of most implementations of algebraic topology – see here, for instance.

• Abstractly, simplicial sets assemble into a (grothendieck) topos, which gives us access to lots of heavy duty category theoretic machinery when working with them.

Speaking of heavy duty category theoretic machinery, this marked the end of section $1$ of the talk. Section $2$ is about the interpretation of HoTT in $s\mathsf{Set}$, and there’s a notable spike in vagueness here. Unfortunately the math becomes quite a bit more technical (and involves a lot of category theory I didn’t want to assume of the audience) but I still wanted to give a flavor for externalizing HoTT statements into statements about $s\mathsf{Set}$. That means I wasn’t able to give many details at all⁴, but I still tried to roughly sketch the ideas involved.

Again, I pointed to the literature for those who want to see things more precisely. There’s an excellent set of three talks by Emily Riehl, On the $\infty$-Topos Semantics for Homotopy Type Theory (lectures 1, 2, and 3), as well as associated lecture notes. They do a good job motivating the semantics in any $\infty$-topos (as the title suggests) at the cost of being somewhat more abstract. There’s also a paper (The Simplicial Model of Univalent Foundations (After Voevodsky), by Kapulkin and Lumsdaine) which works only for $s\mathsf{Set}$, but is much more concrete. I forgot to mention it during the talk, but Subramaniam’s talk in the HoTTEST Summer School Colloquium is another fantastic resource.

Morally, the idea is that types in HoTT are kan complexes (that is, simplicial sets which are “honestly geometric” in some sense). Then constructions on types externalize to (categorical) constructions on kan complexes, and terms inhabiting a type correspond to global points of the associated kan complex.

This is a bit of a fib, since the syntax of HoTT is strict on-the-nose whereas the categorical constructions we do in $s\mathsf{Set}$ are only defined up to isomorphism. It turns out that this is a serious technical obstruction, since we need to choose a particular object from each isomorphism class in order to interpret the syntax. But we need to do this in a way that the constructions are all compatible.

For instance, say $P$ is a dependent type over $B$ and $f : A \to B$ is a function. Then if $a : A$ we could first evaluate $f(a)$ then consider the type $P(f(a))$, or we could first compose $P$ with $f$ to get a type family $P(f(-))$ over $A$, then take the fibre at $a:A$.

No matter what, we end up with the syntax $P(f(a))$⁵, so we get literal equality at the level of syntax.

However, in $s\mathsf{Set}$ if we choose a representative for each isomorphism class, and define our constructions to manipulate those specific objects, it’s possible that we chose poorly so that we end up with different objects depending on which order we choose to perform the above substitutions (they’ll be isomorphic of course, but this is not good enough).

The key to solving this issue is to somehow make one really hard choice, then define all of our other choices in terms of it! This is the idea behind Voevodsky’s (weak) universal fibration, which you can read all about in the linked paper of Kapulkin and Lumsdaine.

Lastly, I mentioned a good exercise to keep in mind when trying to learn this material:

---

All in all, I was pleased with how the talk went, and I learned a ton while writing it! I still have to work through the details of the semantics to fully feel comfortable externalizing HoTT statements, but I have a much more nuanced appreciation for the issue of strictness.

As usual, here’s the title, abstract, and recording.

Take care, all ^_^

---

Where Are The Open Sets? – Comparing HoTT with Classical Topology

It’s often said that Homotopy Type Theory is a synthetic description of homotopy theory, but how do we know that the theorems we prove in HoTT are true for mathematicians working classically? In this expository talk we will outline the relationship between HoTT and classical homotopy theory by first using the simplicial set semantics and then transporting along a certain equivalence between (the homotopy categories of) simplicial sets and topological spaces. We will assume no background besides some basic knowledge of HoTT and classical topology.

You can find the slides here, and I’ll post the recording as soon as it’s up.

Edit:

Here’s the recording ^_^

---