# What is an explicit bijection? (FPSAC 2019 slides)

- 04 July 2019
- 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.

**How to comment on this blog:**At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention

`andrejbauer@mathstodon.xyz`

, I will
gladly respond.
You are also welcome to contact me directly.
## Comments

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

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