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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yw1-xc3d.google.com (mail-yw1-xc3d.google.com [IPv6:2607:f8b0:4864:20::c3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 13d57223 for ; Mon, 1 Jul 2019 11:52:19 +0000 (UTC) Received: by mail-yw1-xc3d.google.com with SMTP id p68sf15358446ywp.2 for ; Mon, 01 Jul 2019 04:52:19 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561981938; cv=pass; d=google.com; s=arc-20160816; b=nBTodeuppMQRfe5dHlLQdAPUDGbLFdSHd4QVKYdA4IhDrNH/PFwJWE63jcyIAFJHcF IdBVp78wybcIi57ulv+zGWOAZ+im5X1SGOXm8FhpM1PPDB2msngzM+2FnrNOpj+oj99s DCBYhk04VpPLj9Qv1Bl4xmuaqWzK543ITM3hq9+6czvUr1Ol9udDOsFrkQxBE2MNErMW xJWKgPvhi9Fw5F5/PTowIysABtr1rAMvXyRZzjLPbe7WC1bVCyU7KyZntCl47irFNyWM B3/OkPY5w5trHdTo/d18lXxmxPR2igQ+OLcbTX53d13Pq3xU/2dAGhcQekLMfRdeog5e 7gwg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=hoZUJv1k+9dDI/cR9i3mfL7lw5mnfWFj2vlScNjQvlE=; b=Hf60zWhUUmkcXlrUpgAuzxXIAxvaefrHAa80ZY18UQ2UUDYsePvZi+dX9XnAlFORsD oVoP7zeYnQ7hrn87EwJ7F801Zn9oLoHExXKQaIK8fzqKdn+90J9S9d7hov3PJ7IsEFT3 xlToUZoMG1oOPZrXzp7+awTgSgHCVSiCnscPrZYi7B+Ed3OhEVJs5kbzuyryBuklwJho PjkGgFeCmAU2zgER/bD0+DfePy4Xa6eQTBCGCY1a95hbWZL2NF+PfHZoME11aE/xS3HL xhVHBVGKn6tjc7P6pJgZR6OgwDZKCXBoOURKpd8KknKNZhwburGL8vmRRhwiCgkgfq5Q xf+Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LKj5hOCs; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::72e as permitted sender) smtp.mailfrom=gabriel.scherer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=hoZUJv1k+9dDI/cR9i3mfL7lw5mnfWFj2vlScNjQvlE=; b=oB97qPjej3FE+QXQj7SImF2YUuXbMyjbJTA2DhC9DYb/mm9eCRzQb/xlmHNjMRGYoK U8e4hIGWHq6ioe/02g94juKFE5nOrroReyTiK4vb8TgxY8fhyJqZkimSAd9CRHoh/Krn GdN42/1ZqHKdI+Q7H/o91ENR80FVuupnz+gK7OM8ks/fCeDmm4lkXtKXrahDRdzmOWzo aSSzfb4LRUOMkvAH1giW1B2Gz91tv7+/koLVnX/ADEuhh/U9WAYtZ7PINkp8OXHYzLfp fMnStS5n0lgq5yigSqxRPAaRHK4qtheiO/klk8Hjwun3j3VxDhyOrbGqx4V6H6/vXlxL eDWQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=hoZUJv1k+9dDI/cR9i3mfL7lw5mnfWFj2vlScNjQvlE=; b=BkDF1bFDzFZThUfxih7Ft/UQD9wlXlXywhJxO2AhVoZorAONGx2u+nfstp+YUqCIYC RBKSmfOA9+ivZSscH3DL+h1nUjH/YLNJ2oNlchbvR6Q6y385uwSEmbMWco1KGKOxzrRd LX8mEGQhSws2SwyCGA+z63cU56PrpZ6Pm02qI/HaSRo3zc9m16tNuB/hEgL7BPROPQJg 4t5L0ip5lytTG1aFAEKlhuQNEMzbiR4okdcJtzZfQemSjR171aPyNgDEG7AhlpfjahaR 24yZJG2VqtDmBSeI0IscbSq748wEfjCW4RcOhJnIXhoi7Rj0kAh7+s6hI0Vu+9r5EDpp Gyzw== 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:references:in-reply-to:from :date:message-id:subject:to:cc: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=hoZUJv1k+9dDI/cR9i3mfL7lw5mnfWFj2vlScNjQvlE=; b=uHlWi0lu16WctlGD0tmAX5m3IEelm4VFFp9N+0X0BPOJcWnCAPAb8sTsUjzngsuxP7 0Br8htUonlx6N7w/XPf6gtmXqCQkYGTpeigIcwvsXXD6d7SPFccKJXT3Gd2KOihSv9Fc phTaJfj8W+Ek5iNKmyK2csE8UFQ4QBw6PUM/kpUuP+eVtvc/bhWqrV5fb4TFW2Z40CXt 7fy/8/+P5n/+7MjGOZ+DcvA1Yw5PgQP6E+YydGPKb8nR5SVYpKXzwlMqKfpGW07SCT/B X/32joKTVeAVIYgTar602aR2Q1JTvcfh/jraKnjywMglL5YQBbzZPmMYE3wlSIvCaZh9 /GbA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUzK/UgO15g3uVj1Qptv9Vpc7RI9luDwV2kCxoMqqDJpfYQquy1 4VQXf/UK1lPa63lIgj1Runw= X-Google-Smtp-Source: APXvYqwFQbwUzRWjECM6ByNjKokXjHqQQ85KyBDsqN4b7RY9g/Vf5wWOlwz7ra0bba8h0+0npH9jJQ== X-Received: by 2002:a81:308d:: with SMTP id w135mr14453930yww.110.1561981938040; Mon, 01 Jul 2019 04:52:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:683:: with SMTP id 125ls1333682ybg.16.gmail; Mon, 01 Jul 2019 04:52:17 -0700 (PDT) X-Received: by 2002:a25:bacf:: with SMTP id a15mr15598708ybk.213.1561981937684; Mon, 01 Jul 2019 04:52:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561981937; cv=none; d=google.com; s=arc-20160816; b=sdjpFKoBtgHEFjp0s89q7dw5twI3JS8B5rvBWSXwXSaNrg7kTYWIyA3u+sqNRBzSgz nzadsCSMDaR3snr3CL1T8IowMM+lUjEhssltnh8TBRQVen291ukdTCxNZfDxMXN91Wsb hR//oeb0bbiQQHGxl2FWPMAKmmg2skeG6BKZNgxohMkzhLqCMrs8al2a5tWKod67PJFR P4skLUGdLt25Gb1BHw652xik5Hpz3fKmHewU2hBm8QKWdfVFQZnGQS+c7MOvt5I+CLFQ Xqjq0zALWER0vdiqsjR0NrkiBop1itWMEMSr3xypFIZEAwcuVh2peWogx3jxsJuz7jpu 2+OA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=cxxMf3Rm3wVLfhYphAjz49Fx94EClHikeBGJ6hgpHgM=; b=FaZLQomz76PVOow+8AUV5+snTtECi+vJz2dDoM/hnaUqc5s3n3yOUadAskO4Gi4TOT Z5vt233dhW6zpo6PxgZkj62OTlOAZGQnYY5Z38Rj8MxJCGQ+CJhEP+YPdGL0MIkoaPX6 l4g1l++6AtnDxgaazCSqZi867/DJt6bZWX/PNCuN7gZN0RCQTQmnWS6wtqnfp5KJ6JH4 mZ1UL8lpdNiHxjpg2D8l8fq+arghlNLGayEXyERqnpmTDkrG3xjW4CtqNVDZHHYoAqw5 5Q8xxJK9UyLDZR9e+juWNvzKR7LRXyDvsjDKGF3tuUQ9DQHrWeUPMeEvBpUOVeu7bcn5 mYyA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LKj5hOCs; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::72e as permitted sender) smtp.mailfrom=gabriel.scherer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x72e.google.com (mail-qk1-x72e.google.com. [2607:f8b0:4864:20::72e]) by gmr-mx.google.com with ESMTPS id q129si139305ybc.1.2019.07.01.04.52.17 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Mon, 01 Jul 2019 04:52:17 -0700 (PDT) Received-SPF: pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::72e as permitted sender) client-ip=2607:f8b0:4864:20::72e; Received: by mail-qk1-x72e.google.com with SMTP id l128so10692437qke.2 for ; Mon, 01 Jul 2019 04:52:17 -0700 (PDT) X-Received: by 2002:a37:2c46:: with SMTP id s67mr20631444qkh.396.1561981937425; Mon, 01 Jul 2019 04:52:17 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Gabriel Scherer Date: Mon, 1 Jul 2019 13:52:55 +0200 Message-ID: Subject: Re: [HoTT] HoTT combinatorics To: Andrej Bauer Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: multipart/alternative; boundary="00000000000086a0ee058c9d4252" X-Original-Sender: gabriel.scherer@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LKj5hOCs; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::72e as permitted sender) smtp.mailfrom=gabriel.scherer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , --00000000000086a0ee058c9d4252 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Not HoTT-specific, some of the recent type/proof-theory work of Noam Zeilberger may pique the interest of combinatorists. For example, A sequent calculus for the Tamari order Noam Zeilberger, 2019 https://arxiv.org/abs/1803.10080 uses a sequent calculus to describe the structure of an order relation on trees that combinatorist have studied, and re-derive counting results on the intervals of that order. (Reasoning on the structure of an order relation is not too far from the "higher" concerns of HoTT and higher category-theory. And the idea of using adequate proof structures to prove a coherence result has been used in many other more categorical settings.) On Mon, Jul 1, 2019 at 1:36 PM Andrej Bauer wrote= : > 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 = "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-finit= e-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. > --=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/CAPFanBECYaoV-WoC8A67LE749%3DZfCQWs%2BSyN9G7mnSvpU6nOfw%= 40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --00000000000086a0ee058c9d4252 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Not HoTT-specific, some of the recent type/proof-theo= ry work of Noam Zeilberger may pique the interest of combinatorists. For ex= ample,

=C2=A0 A sequent calculus for the Tamari order
=C2=A0 Noam Zeilberger, 2019

uses a sequent calculus to describe the structure of an order relatio= n on trees that combinatorist have studied, and re-derive counting results = on the intervals of that order.

(Reasoning on the = structure of an order relation is not too far from the "higher" c= oncerns of HoTT and higher category-theory.
And the idea of using= adequate proof structures to prove a coherence result has been used in man= y other more categorical settings.)

On Mon, Jul 1, 2019 at 1:36 PM= Andrej Bauer <andrej.bauer@a= ndrej.com> wrote:
In a couple of days I am gonig to give a talk about HoTT in fron= t 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 &q= uot;explicit
construction" and "abstract proof of existence".

2. Discuss univalence and how we get "isomorphic structures are equal&= quot;.

3. I will advertise Brent Yorgey's PhD thesis about combinatorial
spieces, and probably cite some gems from it
(https://hom= otopytypetheory.org/2016/07/20/combinatorial-species-and-finite-sets-in-hot= t/)

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 &= quot;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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAB0nkh2h_L_9ANAZdiu%2BZmAXRTi_S7= HQDG9RYCuvYbbVk-HmqA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;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/CAPFanBECYaoV-WoC8A67LE749%3D= ZfCQWs%2BSyN9G7mnSvpU6nOfw%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--00000000000086a0ee058c9d4252--