In a couple of days I am gonig to give a talk about HoTT in front of
250 combinatorialists at
http://fpsac2019.fmf.uni-lj.si
I have some ideas about how to explain that HoTT is relevant to a
mathematician who studies "simple finite objects", but I'd be
interested to hear if anyone has anything else to say. I'll gladly
acknowledge good ideas.
My current plan is to discuss, after a suitable introduction:
1. The difference between Σ and ∃ is the difference between "explicit
construction" and "abstract proof of existence".
2. Discuss univalence and how we get "isomorphic structures are equal".
3. I will advertise Brent Yorgey's PhD thesis about combinatorial
spieces, and probably cite some gems from it
(
https://homotopytypetheory.org/2016/07/20/combinatorial-species-and-finite-sets-in-hott/)
I don't have a good feeling for what might pique a combinatorialist's
interest. Does anyone here?
With kind regards,
Andrej