From: Andrej Bauer <email@example.com> To: "HomotopyTypeTheory@googlegroups.com" <firstname.lastname@example.org> Subject: [HoTT] HoTT combinatorics Date: Mon, 1 Jul 2019 13:35:43 +0200 Message-ID: <CAB0nkh2h_L_9ANAZdiu+ZmAXRTi_S7HQDG9RYCuvYbbVk-HmqA@mail.gmail.com> (raw) 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 HomotopyTypeTheoryemail@example.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.
next reply index Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top 2019-07-01 11:35 Andrej Bauer [this message] 2019-07-01 11:52 ` Gabriel Scherer
Reply instructions: You may reply publically to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=CAB0nkh2h_L_9ANAZdiu+ZmAXRTi_S7HQDG9RYCuvYbbVk-HmqA@mail.gmail.com \ --firstname.lastname@example.org \ --email@example.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: link
Discussion of Homotopy Type Theory and Univalent Foundations Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.hott AGPL code for this site: git clone https://public-inbox.org/ public-inbox