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=-2.1 required=5.0 tests=BULK_RE_SUSP_NTLD, DKIMWL_WL_MED,DKIM_SIGNED,DKIM_VALID,FROM_SUSPICIOUS_NTLD, MAILING_LIST_MULTI,NICE_REPLY_A,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 5316 invoked from network); 14 Apr 2022 20:23:47 -0000 Received: from mail-ed1-x53b.google.com (2a00:1450:4864:20::53b) by inbox.vuxu.org with ESMTPUTF8; 14 Apr 2022 20:23:47 -0000 Received: by mail-ed1-x53b.google.com with SMTP id cx6-20020a05640222a600b0041df79fb9e8sf3634893edb.1 for ; Thu, 14 Apr 2022 13:23:47 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1649967825; cv=pass; d=google.com; s=arc-20160816; b=iycUqzx0cdNNQ/hiDNz7ImuVfSnVhwHeWe4pTm7CB+eEdDlWD6AAIzaV5dATOF9eyf 4Q7mnNPvRrHNS1s68qZVgCNDfEt84HR7HQsTsla5qqojDCes3X768tYG9BNl6xnZJxb+ fzFbzJUT/0KTRGGoLw7D2SqSRGlHGw6X369HFSCAVa30WkhfMazTm/47eI6DxwcoW1sw TCzVUP50608CudaA0P07El/9v0bITapzdSEPM++RuCPbRI16Z4svPhUz9afJq59BysWX Q7mJRwAGhEINmFxQ9VLmXFvCts8JKM10qNbFcYPE61MtiwSVy5o+TdpCZU/SkzzcHuE5 Ob7A== 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:content-transfer-encoding :in-reply-to:from:references:to:content-language:subject:user-agent :mime-version:date:message-id:sender:dkim-signature; bh=D8M6m0nqsh8XGT+GQDXKM4Rn3eR1bmkI87xOxndeaw0=; b=nlpogCvsKFcYJ0TtoOkBTcTUe7s3kYlhEtDqdH4g/u0eka1K4E1QFC0C0HkUvO8hP/ L17NQ02FkSLha1h89GYBIkuZg4JC2yJfSbrTgUso4u0ukL2SEj557VmBWt5haMN9IFC0 o1lwt6O3Ak/QFwfBhsTUKSS+nnA7obKWSofHI/pd3GoCY0YWLgG3aSygYZh7E+w8XxWA 9QP9Na7+SMXP5S2heafZK9jI4btZpEaPSema+NZOQUS4y2+DLZrHDEKtmS53ThxvO1kn amRLs6VyNyOjKXEnE+mdKWyiI3liKcQ5clrt4H548CWUy/yyKUNPH6Iq7MfU/C/Bwsgf ZdBg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=i916xRzZ; spf=neutral (google.com: 64.147.123.21 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) smtp.mailfrom=zero@fromzerotoinfinity.xyz DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:message-id:date:mime-version:user-agent:subject :content-language:to:references:from:in-reply-to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=D8M6m0nqsh8XGT+GQDXKM4Rn3eR1bmkI87xOxndeaw0=; b=s+Fr9ytf9r3y3kRsrTiFEiwOMgONcecdYzbqDbQe+5JDKVcl8RA51dx/B9Hy2gaCLO XKj60VTx9FIYnGjrTqqji1JBxh/0mMiYCrWvZX/WMIcBfmZ/Yn3wihog2G9HqfigKkU5 KFqIAk7i+DMMFIvj65ZFBrN9cgx9kmfxhvLF+ulMOQ05sGtMbWWbvYq46Ebx73zwmFp7 2HFDwQsRd9c4aRDZnSUS+In1g7dCO8rqBbXvu2Ty4/OG6MWdxhohPLN3+WXLXLOSZoTu X3aVzLjWEdVZCM4Ynngc3PvvFjZ0fHCwvLdv1KQh2ZMMe0kw+WrAfwWmfrOttDoBfaiU 7sBg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:message-id:date:mime-version:user-agent :subject:content-language:to:references:from:in-reply-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-subscribe:list-unsubscribe; bh=D8M6m0nqsh8XGT+GQDXKM4Rn3eR1bmkI87xOxndeaw0=; b=exi3zi0Pgc8+Rd7ZXrs3SJT5wKtBC10WMAiHu8sYdMHYbBqHGeJDDyKl7usyBiP5pm KnVuFRwInIxCejXm0oNqJ/ikSgwiPfI9nVkskPf129qbizKYdhYTxGi2dMVo80TFnxQ2 uZJUSLlROPOmFFJFvwc0cDF+vNyCCgMOXfoS/jjxZzbpmm/edKKqkDppE6aw8jWf3/BO xWKO+PKNPw6JEKzZk54RhTLI5thL8xQNDD9MyQOhFowB7idzOIYDX+1HQGHxyGPzy4G+ jdHforJtqMpejNRMr7ogCOo09/PpjKWDxh4Ns8en0OURAM/RwmQ5qRiGhSnNwLo1Jusn paOQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533WPnoqehwRwHCnCpyySO8kl+Pn8CuRLURgeANLP810pL4G4uJ9 OB0rahdXazR/qsTdnZ/teRE= X-Google-Smtp-Source: ABdhPJy7J7y7N8HSru2Rrc4hOGqwjMz927MLxhkV+DFbjkw8RmmA4h2D/Kes7lDNuyD7DDpWYboC6A== X-Received: by 2002:a17:906:9b85:b0:6db:ab80:7924 with SMTP id dd5-20020a1709069b8500b006dbab807924mr3837146ejc.160.1649967825027; Thu, 14 Apr 2022 13:23:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:907:8a0d:b0:6e8:c7a3:5746 with SMTP id sc13-20020a1709078a0d00b006e8c7a35746ls3145316ejc.6.gmail; Thu, 14 Apr 2022 13:23:43 -0700 (PDT) X-Received: by 2002:a17:907:1623:b0:6df:c9da:a6a8 with SMTP id hb35-20020a170907162300b006dfc9daa6a8mr3739730ejc.303.1649967823197; Thu, 14 Apr 2022 13:23:43 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1649967823; cv=none; d=google.com; s=arc-20160816; b=ArPlp/xRlvlmk3xNQQcsbhvkCqtH3JOF6jBVsm0woYY2Ay6hOPQ96+2ulJBaoj3Tfk s1/O768lY2YicUp37E8RxSDw1okARLWA1J/PZBoBE/zzRnaCg03wE5cJ9z2HfttZRQ5v CSP/wwF1UHea0LxhSDYXHbLrTThcIdF2AsQdG5/cLfmCL3xU/xunSoX83OcW69M5GdpN VPcQBx5/WevMgK2v/WGX+GbFnqBrhb+MupP3hR4x8oeCGtZhWZRVjck/i2z5XS4RAuOU Zh9drDBwKhZn95c9NVHap0ck2rCMJaKPIbPgqT045m8Bs7lxyZbWJu1Sz6gSZQfn3aIM O5KA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:in-reply-to:from:references:to :content-language:subject:user-agent:mime-version:date:message-id :dkim-signature; bh=dwp1E+dvZbYlSuzNKt0fYZpofZH9/0pNr0s5c7WE10A=; b=0d9EeL4VC30uX3TVoXWFGbwIpxaB+lMpTYUVeaZ1Yv5a93JbiLs6tFRusjSGawNogq 06lhwfoHFl8mJVOUoN1VB39Uf08sijUUYvtz5azGdHiWaYGaukNZywdqtc73UySpG7S/ i2/Q4JLZFibfJFjNsR5LaW8cUjByv8HfNp69C3B6lz+EUGclX44jfQ0IuhOmu0Vt2e+I iZVq4XKvIJJfMrKVrG+NxPJvq7I9p/8N/tJjI+R1jHTMrXWfeD4zy04594wR0suR1K7J MAJGqlXNNh/QeNuspLiEr/tdB9A+DKFcnyoEiAVb9f410jLXiOp6Xfe7RYVlJlezxnku LVXQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=i916xRzZ; spf=neutral (google.com: 64.147.123.21 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) smtp.mailfrom=zero@fromzerotoinfinity.xyz Received: from wout5-smtp.messagingengine.com (wout5-smtp.messagingengine.com. [64.147.123.21]) by gmr-mx.google.com with ESMTPS id c8-20020a509f88000000b00415e600c761si445374edf.2.2022.04.14.13.23.42 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 14 Apr 2022 13:23:43 -0700 (PDT) Received-SPF: neutral (google.com: 64.147.123.21 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) client-ip=64.147.123.21; Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.west.internal (Postfix) with ESMTP id 1CB65320278C for ; Thu, 14 Apr 2022 16:23:41 -0400 (EDT) Received: from mailfrontend1 ([10.202.2.162]) by compute3.internal (MEProxy); Thu, 14 Apr 2022 16:23:41 -0400 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvvddrudelfedgudehtdcutefuodetggdotefrod ftvfcurfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfgh necuuegrihhlohhuthemuceftddtnecufghrlhcuvffnffculddujedmnecujfgurhepkf ffgggfuffvfhfhjggtgfesthekredttdefjeenucfhrhhomheppfhitgholhgrshcutehl vgigrghnuggvrhcuufgthhhmihguthcuoeiivghrohesfhhrohhmiigvrhhothhoihhnfh hinhhithihrdighiiiqeenucggtffrrghtthgvrhhnpeevhfehgfeuffffueegudetjedt hfeiheegfeegledtheelieehkeeivdeghffhvdenucffohhmrghinhepiihoohhmrdhush dpuhifohdrtggrnecuvehluhhsthgvrhfuihiivgeptdenucfrrghrrghmpehmrghilhhf rhhomhepiigvrhhosehfrhhomhiivghrohhtohhinhhfihhnihhthidrgiihii X-ME-Proxy: Received: by mail.messagingengine.com (Postfix) with ESMTPA for ; Thu, 14 Apr 2022 16:23:39 -0400 (EDT) Message-ID: <876f6e58-211c-4824-e938-4b915e18d859@fromzerotoinfinity.xyz> Date: Thu, 14 Apr 2022 22:23:37 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.7.0 Subject: Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Content-Language: en-GB To: HomotopyTypeTheory@googlegroups.com References: From: Nicolas Alexander Schmidt In-Reply-To: Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable X-Original-Sender: zero@fromzerotoinfinity.xyz X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=i916xRzZ; spf=neutral (google.com: 64.147.123.21 is neither permitted nor denied by best guess record for domain of zero@fromzerotoinfinity.xyz) smtp.mailfrom=zero@fromzerotoinfinity.xyz 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: , Dear Chris, with great interest I saw the advertisement for Mike's upcoming talk.=20 When I saw that the announcement had spawned a proper thread, I of=20 course assumed it was because of the interesting mathematical content. I was greatly disappointed to learn that the reason was not mathematics=20 at all. Mathematics, like any endeavour, can only thrive when it is a=20 meritocracy. You don't have to like someone or agree with his political=20 views to appreciate his ideas. And Mike is one of the best people in the=20 field, if not the best. So, why are you trying to cancel him, Chris? Are=20 you trying to advance your own career? By cancelling him, by preventing him from disseminating his ideas, you=20 are damaging the whole field. Don't pretend that you're making a=20 "difficult decision" when you are acting selfishly and reprehensibly. Best, Nicolas > 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. > > 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. > > Carlo Angiuli > Dan Christensen > Chris Kapulkin > > On Mon, Apr 11, 2022 at 9:32 AM Chris Kapulkin wro= te: >> 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. >> >> Each lecture will be one-hour long and will be followed by a 30-minute >> discussion. The title and abstract are below. >> >> The Zoom link is >> >> https://zoom.us/j/994874377 >> >> Further information, including our Google Calendar and Youtube >> channel, is available at >> >> http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html >> >> We are looking forward to seeing many of you there! >> >> Best wishes, >> Carlo Angiuli >> Dan Christensen >> Chris Kapulkin >> >> * >> >> Mike Shulman >> University of San Diego >> >> Towards Third-Generation HOTT >> >> 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. >> >> 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. >> >> This is joint work with Thorsten Altenkirch and Ambrus Kaposi. --=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/876f6e58-211c-4824-e938-4b915e18d859%40fromzerotoinfinit= y.xyz.