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

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.

Video recording of the lecture is now available.

Cym13

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.

Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.