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
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
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
these form an adjunction (
- They induce functors on the homotopy categories
and form an adjoint equivalence
The punchline is that any question2 we have about the homotopy theory of
topological spaces can be answered by transporting to
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
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
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
For instance, say
No matter what, we end up with the syntax
However, in
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:
Can you show that if HoTT proves
After this, can you show that
the geometric realization
If you can do both of the above exercises, you’ll have successfully proven a fact about an honest topological space by proving some theorem in HoTT!
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 ^_^
-
With their usual model structures ↩
-
Well, any question that transports along categorical equivalences… But that means every question we can phrase categorically!
This is part of the reason so many category theorists get a bit obsessive about phrasing everything in terms of category theoretic jargon. It’s not just to make life hard for people who don’t know the lingo (even though it might feel that way), nor is it just to help us organize our own thoughts and relate different constructions to each other (though that’s a big part of it). One big reason to go through with the endeavor is to be able to transport as many things as possible across an equivalence of categories, and things phrased in a categorical language are automatically invariant under these equivalences! ↩
-
In the questions and discussion after the talk, Dan Christensen mentioned an important point: This equivalence goes much deeper than just the homotopy categories. In fact, we get an equivalence of
-categories between the simplicial localizations of and at their weak equivalences, which tells us that much more homotopical structure is preserved by this translation! For instance, the mapping spaces.On the one hand, this is great (since it means our translation is even better than my talk lets on) and necessary (since this higher structure is useful when working with the semantics of HoTT in
).On the other hand, it requires one to say the words “
-category”, which I was trying to avoid for concreteness reasons (and because I’m less comfortable with them).I figured I would mention it here, though, since it’s a lot easier to have footnotes and asides in a blog post than in a talk ^_^. ↩
-
Though this ended up being good for time-management reasons as well. My talk was basically 30 minutes on-the-nose, which I’m pretty pleased with to be honest. It was pretty ambitious, and I’m glad I managed to stay on time!
This was also good because I’m less comfortable with the translation from HoTT into
, and glossing over details saved me from accidentally saying something false. ↩ -
Or, if you want to be extremely precise,
. ↩