What is an explicit bijection? (FPSAC 2019 slides)

• 04 July 2019
• Andrej Bauer
• General, Type theory, Talks

Here are the slides with speaker notes for the talk What is an explicit bijection which I gave at the 31st International Conference on Formal Power Series and Algebraic Combinatorics (FPSAC 2019). It was the "outsider" talk, where they invite someone to tell them something outside of their area.

So how does one sell homotopy type theory to people who are interested in combinatorics? That is a tough sell. I used my MathOverflow question "What is an explicit bijection?" to give a stand-up comedy introduction, after which I plunged into type theory. I am told I plunged a little too hard. For instance, people asked "why are we doing this" because I did not make it clear enough that we are trying to make a distinction between "abstractly exists" and "concretely constructed". Oh well, it's difficult to explain homotopy type theory in 50 minutes. Anyhow, I hope you can get something useful from the slides.

Download slides: what-is-an-explicit-bijection.pdf

Video recording of the lecture is now available.

Comments

Cym13

09 July 2019 at 09:13

Hi, the PDF is nice to have but do you know whether your talk was recorded? I would love to watch your talk!

Andrej Bauer

18 July 2019 at 09:40

The talk was recorded by videolectures.net. I will add a link when it appears.