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

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

##### Post a comment:

`$⋯$`

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.
## 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.