From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 21794 invoked from network); 15 Apr 2022 03:00:15 -0000 Received: from mail-io1-xd3c.google.com (2607:f8b0:4864:20::d3c) by inbox.vuxu.org with ESMTPUTF8; 15 Apr 2022 03:00:14 -0000 Received: by mail-io1-xd3c.google.com with SMTP id w28-20020a05660205dc00b00645d3cdb0f7sf4111574iox.10 for ; Thu, 14 Apr 2022 20:00:14 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1649991612; cv=pass; d=google.com; s=arc-20160816; b=dHAPeaMag0QXszSgznfbYxx/9ST70oIJ69Nw1V6G3rhfwRwbh9aRyNBn8JAlddKQV2 pgsd/qYzXDienTXkveoRl1UQWpn7sZFdEAoXj58r8dlTvvpfFe6Q84YAlq0oBVaZTTCS OVUxFxcr44B4hfgGQItFZfsbXu978Nw44oM5SeFuoIc9Gh3MplxBPyuDI7ClmcNK/roL R3pZaN+VDtCTwZkoITS4xylp7JWWjG7/f2CRUR+AGKUWYctz+zpvl8d6L+MflMJsmgNj aRFyMfRD7iPZDFP37jkodAKonP2RSS+Ug95OBflU/2gBFw2xxeRuCpozH7HjsLb9V2Se erpQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:message-id:in-reply-to:to :references:date:subject:mime-version:content-transfer-encoding:from :sender:dkim-signature:dkim-signature; bh=PGG6LxLE4Hey0pvd3XrIlyUWMGmkZ++tP8bH1RatW6E=; b=wQsYSKEH+0o1XX8sTsbcwt6uZRRc3wsfGMYyQPUFq6q/LDP3zzbJ/hRS/XR2U623kA k3sisEB5XgfHalFziLqBIZjUonRTuymlI+2qGjFRaoFx6jbWN7vAJfac+O7dpdSh47sm 9FCme3wSkURoG9P5RMPZJiGUfJTgnISQeiiOmQyyW+wVy3r89Z6fd+HdDedmYCMfdlbW xwMi36wpIC6hLhuG9sZz4m1W6BrNFhOtPMtXsqgUIcgz6jf5F8kLoJCpQoAUeedD3ghY 3PHD++B8ZqzNlQ4s6WAa9nCochE/jJP3tJLuhb+8httJ5N7t4VmS6kTDNVsnBUJTKgiY vFVg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=gRFiz+sm; spf=pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::1029 as permitted sender) smtp.mailfrom=axhkrz@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=20210112; h=sender:from:content-transfer-encoding:mime-version:subject:date :references:to:in-reply-to:message-id:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=PGG6LxLE4Hey0pvd3XrIlyUWMGmkZ++tP8bH1RatW6E=; b=jy/VCpnhIPciP8P9LO6Oo2f0R+3lShsohjHLl93U7qGfTXPSG1mSqLaXcNsUuUOtzE pW2R9HiyrBbgPufcLQdHlaE66N4sqhn/Cic0xiD+nYzMMgKaiIiDs+hkjRoSb4k8DITi JgsUXDZGlJOqQ3YDWRgyc/O/QD8h7X28HwaqxZEAtkTQugHoth2r/jUSAV5D1l+y4Uiz bwydqgukypiLFgay4OZvEE3nU6Nf0PM7Uu3tTJ38u8R3EqRVQ/v62yKqW0gFh+UY2AKW QtwCHtlfYwGDlHffWT0bYosX3m/jCEtFqOz/57xtug5u7kavME6/7SHhnpmZlAyJzw6p 90YA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=from:content-transfer-encoding:mime-version:subject:date:references :to:in-reply-to:message-id:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=PGG6LxLE4Hey0pvd3XrIlyUWMGmkZ++tP8bH1RatW6E=; b=W9mFl4UYgQSHSetr1RJkTrLm59Wf7COdSQUl5IvFoxxBk+Ds0fnjzs3IzfNoRhRg3b Z2AyIT6m3O/9XCNGkPuFQ0d6KWso7/qggwPrWc7VD6D+hZwMiEe03eyN28Zy2lep5ZVn DZBLo7GuW215IXjm2quA70Zt5mlYT1YQXoYwYN97vua6HH8K7jFJQTA0BP1f0cq+9Emi 0B6n8SYWuLu0OOGEHlVVdPpJr4TK22SBIndNpFs5KGlO/ANCDpScRj8SnFOM4S/sK5mH QQYMHhYVQ/zTcTXrwN1WXPXqGh27AgqEuLlYcsXDiDiZxWjcnJlMukX8jtEuWyvn70QK h5fA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:from:content-transfer-encoding :mime-version:subject:date:references:to:in-reply-to:message-id :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=PGG6LxLE4Hey0pvd3XrIlyUWMGmkZ++tP8bH1RatW6E=; b=JYqqs2eChtuffMW89ZM8JX/zheAVxCmjXjx8yTFHUtaTCwuS5DfvHVEdO/S90f918m XqYmMkrmTCOFOXXO89TeqThh3l3YsJ8j3EjLaDGgFRrmV6R6hGntljKDoOPXma/dApzf 0JuA6wRzsh5HG5fzaaBma9GNT8D4XnNoOnYWwh8Yn7BkP7tj4abjTQUFFm7TAdWsuMSZ qWo5cIev27jwuIGhw/Tr2hLX1E9pKIFCB5XgIzyXGJ+NczJYje5piGyiF0Ak+3i8p1ID BrIPOeT7Vs9RUzJfeWh+ZAUpSHzNvfpFm/dICUO/TTaTQUkpbrRRYoQDgxZ/YsB8ID6S OeJQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530EsLfVbCNI7GfKLtx04I/yII7kdlbu4DwyLLjRzRr7sP+LOnaW aYIAkeU04ld0a1fdUwdnjPk= X-Google-Smtp-Source: ABdhPJzh1ofgD5STAOuBYahflqKEYOsgVH/CZ9jfz4hXUpZSyXPqT9Htu42nAQkoiCQBukfcY12b8A== X-Received: by 2002:a05:6638:1408:b0:326:31b6:d92d with SMTP id k8-20020a056638140800b0032631b6d92dmr2803684jad.133.1649991612078; Thu, 14 Apr 2022 20:00:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:d942:0:b0:2ca:c0e9:dfa5 with SMTP id l2-20020a92d942000000b002cac0e9dfa5ls2043758ilq.1.gmail; Thu, 14 Apr 2022 20:00:11 -0700 (PDT) X-Received: by 2002:a05:6e02:1524:b0:2cb:e2c9:672b with SMTP id i4-20020a056e02152400b002cbe2c9672bmr2352456ilu.184.1649991611186; Thu, 14 Apr 2022 20:00:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1649991611; cv=none; d=google.com; s=arc-20160816; b=PmZilVQm7NsLU4SgXRKrmpKZxwiK8t622pC94sWqF3mREnMNCDReQ0LwpnMo38soCS Wu5jTyJQ8K1AZwwv95UTjrlS8bkd8sOfVTpwkk3d8xtdAAfdPe7vI2UXcA0eR0uSpk69 g+ZM7Oc9BjuheC2HbcMoI8rZwds8cddJzveF1HvZCihmSTi+lOUF8p37EgnwNJSmnhXQ qB0v6nhdKYNu30GZ7Hjs2GNgYQENHPI/dc5iiNdXr/9AczXxfdzxOBK7BYcMJtaLOnUr MjpSYaaOzqU5mZ1EIHFMEc7ng0Mqsj+U888SYW6g0cVGl5EiC01jg4wgaX/tgSqvNkYf Fltw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=message-id:in-reply-to:to:references:date:subject:mime-version :content-transfer-encoding:from:dkim-signature; bh=YrQUZQ4hgKFatG85k98BEvDubZIHIk6OxSQPKgyLJpM=; b=ZeCzbTwwNISW0JJM8iQLMvfSXDdMOTyos3bQpqTXjzCzdlm0b9XkUmS9y/PUIzi//k ChecKO03K/oiBnsqrnJnf3BUeYpdibRzrez5PWIZNRmFi3F5nuq7W04B0kg3fnHSb+3G Y4B/YMVehpHtnl9FJZNX20mi34Dzu9UAiwjSFtuGYWECLbJGDwCswGDIDc75fZKx2nL5 xbuawApKCooqJ6mBcariZ5NqkRamrZqQ6t+33QX52vnGE/dmPtxunS02uGDcIuVMRPSZ oaHasP8EE3UlJf9VAVoqJSXRsX+iVhd8m/i42d/lFNvjLWn9eIxbmASiE8PiTlIOTWr9 824w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=gRFiz+sm; spf=pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::1029 as permitted sender) smtp.mailfrom=axhkrz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pj1-x1029.google.com (mail-pj1-x1029.google.com. [2607:f8b0:4864:20::1029]) by gmr-mx.google.com with ESMTPS id f15-20020a02700f000000b0032660e40516si21534jac.2.2022.04.14.20.00.11 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 14 Apr 2022 20:00:11 -0700 (PDT) Received-SPF: pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::1029 as permitted sender) client-ip=2607:f8b0:4864:20::1029; Received: by mail-pj1-x1029.google.com with SMTP id j8-20020a17090a060800b001cd4fb60dccso7374145pjj.2 for ; Thu, 14 Apr 2022 20:00:11 -0700 (PDT) X-Received: by 2002:a17:903:11d0:b0:155:c240:a2c0 with SMTP id q16-20020a17090311d000b00155c240a2c0mr49944874plh.143.1649991610683; Thu, 14 Apr 2022 20:00:10 -0700 (PDT) Received: from smtpclient.apple (2603-8001-4200-4757-dc15-c21e-2177-80c0.res6.spectrum.com. [2603:8001:4200:4757:dc15:c21e:2177:80c0]) by smtp.gmail.com with ESMTPSA id b2-20020a6541c2000000b0039d1280084asm2983680pgq.26.2022.04.14.20.00.09 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Apr 2022 20:00:10 -0700 (PDT) From: Alexander Kurz Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 15.0 \(3693.60.0.1.1\)) Subject: Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Date: Thu, 14 Apr 2022 20:00:07 -0700 References: <876f6e58-211c-4824-e938-4b915e18d859@fromzerotoinfinity.xyz> To: HomotopyTypeTheory@googlegroups.com In-Reply-To: <876f6e58-211c-4824-e938-4b915e18d859@fromzerotoinfinity.xyz> Message-Id: <6A66F50E-FAF2-4C31-ABA9-835ED4FDE345@gmail.com> X-Mailer: Apple Mail (2.3693.60.0.1.1) X-Original-Sender: axhkrz@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=gRFiz+sm; spf=pass (google.com: domain of axhkrz@gmail.com designates 2607:f8b0:4864:20::1029 as permitted sender) smtp.mailfrom=axhkrz@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: , List-Unsubscribe: , I would love to hear Mike's lectures. All the best wishes, Alexander > On Apr 14, 2022, at 13:23, Nicolas Alexander Schmidt wrote: >=20 > Dear Chris, >=20 >=20 > with great interest I saw the advertisement for Mike's upcoming talk. Whe= n I saw that the announcement had spawned a proper thread, I of course assu= med it was because of the interesting mathematical content. >=20 > I was greatly disappointed to learn that the reason was not mathematics a= t all. >=20 > Mathematics, like any endeavour, can only thrive when it is a meritocracy= . You don't have to like someone or agree with his political views to appre= ciate his ideas. And Mike is one of the best people in the field, if not th= e best. So, why are you trying to cancel him, Chris? Are you trying to adva= nce your own career? >=20 > By cancelling him, by preventing him from disseminating his ideas, you ar= e damaging the whole field. Don't pretend that you're making a "difficult d= ecision" when you are acting selfishly and reprehensibly. >=20 >=20 > Best, >=20 > Nicolas >=20 >> The organizers of the HoTT Electronic Seminar Talks are committed to >> the diversity and growth of homotopy type theory, and want everybody >> to feel comfortable and welcome in our community. >>=20 >> We believe the speaker=E2=80=99s recent statements in the context of the= HoTT >> Book stand in opposition to these values, and have made the difficult >> decision not to hold the upcoming HoTTEST Distinguished Lecture >> Series. >>=20 >> Carlo Angiuli >> Dan Christensen >> Chris Kapulkin >>=20 >> On Mon, Apr 11, 2022 at 9:32 AM Chris Kapulkin wr= ote: >>> We are delighted to announce the inaugural HoTTEST Distinguished >>> Lecture Series to be given by Mike Shulman (University of San Diego). >>> The series consists of three lectures which will take place on April >>> 14, 21, and 28 at 11:30 AM Eastern time. The Eastern time zone is now >>> observing daylight saving time, making it UTC-04:00. >>>=20 >>> Each lecture will be one-hour long and will be followed by a 30-minute >>> discussion. The title and abstract are below. >>>=20 >>> The Zoom link is >>>=20 >>> https://zoom.us/j/994874377 >>>=20 >>> Further information, including our Google Calendar and Youtube >>> channel, is available at >>>=20 >>> http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html >>>=20 >>> We are looking forward to seeing many of you there! >>>=20 >>> Best wishes, >>> Carlo Angiuli >>> Dan Christensen >>> Chris Kapulkin >>>=20 >>> * >>>=20 >>> Mike Shulman >>> University of San Diego >>>=20 >>> Towards Third-Generation HOTT >>>=20 >>> In Book HoTT, identity is defined uniformly by the principle of >>> "indiscernibility of identicals". This automatically gives rise to >>> higher structure; but many desired equalities are not definitional, >>> and univalence must be asserted by a non-computational axiom. Cubical >>> type theories also define identity uniformly, but using paths instead. >>> This makes more equalities definitional, and enables a form of >>> univalence that computes; but requires inserting all the higher >>> structure by hand with Kan operations. >>>=20 >>> I will present work in progress towards a third kind of homotopy type >>> theory, which we call Higher Observational Type Theory (HOTT). In this >>> system, identity is not defined uniformly across all types, but >>> recursively for each type former: identifications of pairs are pairs >>> of identifications, identifications of functions are pointwise >>> identifications, and so on. Univalence is then just the instance of >>> this principle for the universe. The resulting theory has many useful >>> definitional equalities like cubical type theories, but also gives >>> rise to higher structure automatically like Book HoTT. Also like Book >>> HoTT, it can be interpreted in a class of model categories that >>> suffice to present all Grothendieck-Lurie (=E2=88=9E,1)-toposes; and we= have >>> high hopes that, like cubical type theories, some version of it will >>> satisfy canonicity and normalization. >>>=20 >>> This is joint work with Thorsten Altenkirch and Ambrus Kaposi. >=20 > --=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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/876f6e58-211c-4824-e938-4b915e18d859%40fromzerotoinfin= ity.xyz. --=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/6A66F50E-FAF2-4C31-ABA9-835ED4FDE345%40gmail.com.