[HoTT] HoTT combinatorics

[Andrej Bauer <andrej.bauer@andrej.com>]

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

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB0nkh2h_L_9ANAZdiu%2BZmAXRTi_S7HQDG9RYCuvYbbVk-HmqA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.