From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vs1-xe3d.google.com (mail-vs1-xe3d.google.com [IPv6:2607:f8b0:4864:20::e3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5ff6ab69 for ; Mon, 1 Jul 2019 11:36:03 +0000 (UTC) Received: by mail-vs1-xe3d.google.com with SMTP id d139sf4281709vsc.14 for ; Mon, 01 Jul 2019 04:36:02 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561980961; cv=pass; d=google.com; s=arc-20160816; b=Dwe4G9MXw6WuBNeuDxYiIIEZEmFll154fjwsmxn6LK4Hw2cXhvEGxVI7gGbs3+MOHe 4Eai17HcqDy/FT0ma1f830aT8HOjar1UUjYvGOjbbO2RAl6co+HF5+6fxMo0v5pf8Upc cjU1yDdWMVKc8Dcpzq7kluA/B/kjrfXAsa6D2AkqlTqVbrXuhPwxEpYQJ4EcdjrYPWSq KjxKJWCDluAXM/Tp/qpeJ76aVYKx8dVng2fls5ZnKM3f1N5TlgO7gwNO6yrPq3OafByD GS+fcC4vdim/Ikzfq30gR8wwjhD9EQ4PZrSlofq3vnPL2oUlpHRQZU1J6zlmD25KCgq9 h6dg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:to:subject :message-id:date:from:mime-version:sender:dkim-signature; bh=wlwc1uFkG2LsG+E5VPVTmxjonN2skUf/uuPmk7V3X5o=; b=0+5T0JT37ChinO5vTyYfCZkHnZQSAzVQYr3oNNaR0qjuGOU5CEFlhMJNttqp25QR8f VccfacLXLdyMyoznqQ2pw3V4QpydX5vT9nFJdNHVw+LOtnZWPghaoq8iGh9uowGToR2E Jvvjj2m6tvnfZzITfoweujwn7A3Zni+EI9oq4Q8YhRadgGhE4cHnVJ1LdDSNW2x5v7AA Ixn04znKDgAnMH1nmtgoVBFtvwjMVF/b12D0trtnIzatJbzDQk5Mp8zPMBAFeT0S4YVz pX49NQxhmm9fzhTbIyrvJuP8mJ2OB+zvJxYSxJedHwGVFxFSWhq/lw8jmRzXcOZOcAvB t4cA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=e5DcWJuA; spf=neutral (google.com: 2607:f8b0:4864:20::d2f is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=wlwc1uFkG2LsG+E5VPVTmxjonN2skUf/uuPmk7V3X5o=; b=AubwEe/abURAWC2UkJB+xNfFG2gZb0FZuHp96ZTxAMup/1emXdSFfgynhJM4K0myo4 XY2UINvp50ec01DsJpZA7CPwra5P48PAE7+DCKzsvm/M3gTtvh4zm9EMC3bMNqYiUB1Z I7iQgjDVmSgnNSTWNsJP2u5jg4EdXywxpST590V9v9MxmhHKFE4EgVIEsZCfX2qEnGs3 us5lfMYRzTkKehkdvfgdFH/wNW+cywQ2inxjicm/sHiesk7g66AyzwrnKOA46dgqM+D8 ve3wbDiAUUnMM9NSXai7+J5CkIY6XruBJpqNbVAKVsnd1Ei+Re/E35oWrfs/s2dgrdt3 emxw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=wlwc1uFkG2LsG+E5VPVTmxjonN2skUf/uuPmk7V3X5o=; b=UzmAyWSquIFnLRrrPbilKVkjHqfn28+AiTcWE5br3fYu7hSXoP+hjyOStt2JXxSVFR +s4G3pBkrBiaKDRr/pL1KZ1PLbI5XZoM4/nAHYYhuK1UTv5dl60BW1luJiyppKwt/Rp3 Qfe2qeiiw98L5JIzGw/eocxy1NlD7WEgsE7WfbwIZN1cyfB+/2u47OEfo2blIuvxX0L0 NLy1EbPdYE2Pc9j0McxJnYXGvIXj+qtZDBvLWZVbngTZcgBN/W+V5aMqaqgURmT7jgM2 mjLF2A6cUXlLDNpLE5o/nsz+2CslSMQeI9oc5FCs8eBdqzI3j9lTQbU1eRtMePtpMwpf WKjg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV6mi1m77V1yq53HSxaOJMEV9ZjNrS/mmH8AWMSS/7bK12iGbFt kjHjFSykqypZ0+9X6x7jsJk= X-Google-Smtp-Source: APXvYqxiOuPLsT4HQcU4dqIlGjgOymmkif0kbjAUG9fx6OPTTsc9EXtXFEVYvsCBoKArn8K7fogw0w== X-Received: by 2002:ab0:30c7:: with SMTP id c7mr7680604uam.143.1561980961813; Mon, 01 Jul 2019 04:36:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:5004:: with SMTP id e4ls241394vkb.6.gmail; Mon, 01 Jul 2019 04:36:01 -0700 (PDT) X-Received: by 2002:a1f:b48e:: with SMTP id d136mr8079892vkf.57.1561980961434; Mon, 01 Jul 2019 04:36:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561980961; cv=none; d=google.com; s=arc-20160816; b=P4FtxpoH51xj7vxdh/L07tW8oasE2f4CqE6aKoy+ECSmPjhNNzi0lazFlrVbu/uRyu /Aa1EuUJ04v7KGdwulERQ/5sy+gf2gLxCIRNWdFH8tfPDAC2U+eUqI5SypGChA6TIbC2 nBwctIWSik8GHTRg+1MUwegfusGsMK/9aalCPbTxyshttF40SlHIoKKRLA67oV8yOJOJ t3zrMEb/EoKg8dDx2IP66xjTJvCf6M9O2FcwQNn3MjSG16NxttOAbTrKfdQ6elPJ9rj6 FhjvzeQkwSM9/4qIE5Qxqs0UAc0vgLroFynZQMa+TuKE25Sdl3M3+e7EqOOCPXQbhxxk DABA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=dh5WcnrOv2bOBD3OChStd4SO7VRHEFmkmc6lw00qVY0=; b=IR8ON8UqKYpxUwBbF+pxz/nasMGGy3HGy4DVrVc4RGAjbXKuPCY+SBPhEV5owFB9NS gpJL3awCGla0D8ldLXYFaMofKPhAiPCZotPZHxX6ARWorjXJH33J+vPOy68Zzv24iHKV JhW1dQ8sM2d5Q5UlR3K7OzjZMYh0lDBWdK4Nk1PVLG8QeeXagncqJegFMKjD/RXspZmc l9NVXLN/X0082JTJ4HbS6VHv5lrdkrjngRt2bVZwbGKVJ2CqmtGuhAZhOxdMj3IyaJiE tJZ8SC89ldfPL3w3LmtXuS2lPz0dRV9f0uvpZ1m7UbXmFP1zW2SSxZn5cl9Z66SDsqj3 idyQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=e5DcWJuA; spf=neutral (google.com: 2607:f8b0:4864:20::d2f is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com Received: from mail-io1-xd2f.google.com (mail-io1-xd2f.google.com. [2607:f8b0:4864:20::d2f]) by gmr-mx.google.com with ESMTPS id 63si708979vkn.0.2019.07.01.04.36.01 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Mon, 01 Jul 2019 04:36:01 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::d2f is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) client-ip=2607:f8b0:4864:20::d2f; Received: by mail-io1-xd2f.google.com with SMTP id n5so27978183ioc.7 for ; Mon, 01 Jul 2019 04:36:01 -0700 (PDT) X-Received: by 2002:a5d:948f:: with SMTP id v15mr16812916ioj.93.1561980960821; Mon, 01 Jul 2019 04:36:00 -0700 (PDT) MIME-Version: 1.0 From: Andrej Bauer Date: Mon, 1 Jul 2019 13:35:43 +0200 Message-ID: Subject: [HoTT] HoTT combinatorics To: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=e5DcWJuA; spf=neutral (google.com: 2607:f8b0:4864:20::d2f is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , 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 =CE=A3 and =E2=88=83 is the difference between "e= xplicit 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 --=20 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 e= mail 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%40= mail.gmail.com. For more options, visit https://groups.google.com/d/optout.