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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 21685 invoked from network); 15 Apr 2022 11:22:03 -0000 Received: from mail-wm1-x33b.google.com (2a00:1450:4864:20::33b) by inbox.vuxu.org with ESMTPUTF8; 15 Apr 2022 11:22:03 -0000 Received: by mail-wm1-x33b.google.com with SMTP id n22-20020a05600c3b9600b00390f438260dsf1150797wms.1 for ; Fri, 15 Apr 2022 04:22:03 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1650021722; cv=pass; d=google.com; s=arc-20160816; b=wWH58/eU+G6eJ/WkmPghQPSVuyfo+nqZRSvxgIVI5DpF/2/GboS1d6If4EmNNuSeS9 eIi6HquddxtnCBDZid7bpcOCcFzVtivSnjrEuCZbMkGKOhjNeAVy9nU0WJHuqmEBHJ6Q Xdk0jPKAk7nMzipPdA36hz5kGEZ5SP32BqxfM+ae7ugJNLRfnrn5u8vyJSdX8Hv8SbOn JO5bD3C8ibnDCDsI/1JVKYE1ROHhNvRHii3EUtNFfuQF91Qus0F5iVVJy2qT+Op08ANg YelQRztkfPKO/SjlcDFY21RKO4+JPFHpyTc8e2tZ3rbsW53vOujxdss0oTRMvOOihYTj AjNw== 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:to:in-reply-to:cc:references :message-id:date:subject:mime-version:from:content-transfer-encoding :sender:dkim-signature:dkim-signature; bh=nSouztIGljQ7wgaG4sbHScReSAZxmraLrIcLGbzVNAk=; b=adlj6c+P2xU67s49rZdUleCmzAPmDbxm9k3I77qejMmgeoJyEAixes7lou2G+XHBoo HZjI8V6cce1MTBJMDYal9euVDe47mEfuzLPVnF7VuZJAnobf9KDb1du/g81+1fvLSJrr aBBvVd22w0xas/FEZjkBjtCrt+tKcgH3kl4JpdYZzIT6CyHXSbtggqeSO/6/9dp5vMAw 13XSdqp+gwkB4Y9UvFydyBXYtN7cqnR1Pr4ex2HEsWrQqLMZR/W4pQSRmGppmOns92b7 /aj866cpQJ0YdT4N464WEpO11fH5l/D79J7KVZAO5VuvZfenr2a9knqB9D0UXePGFT/C LjJg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=eRESr8ZL; spf=pass (google.com: domain of ondrej.rypacek@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=ondrej.rypacek@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:content-transfer-encoding:from:mime-version:subject:date :message-id:references:cc:in-reply-to:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=nSouztIGljQ7wgaG4sbHScReSAZxmraLrIcLGbzVNAk=; b=HiWCPLIH5D3bRjLieMnu2oB/1wLhaJ2M4VPP+SjjIZc49QMYXuyQEGu8P9CEZL0/Fu L/nSjGMVnciQGrLmBBt0acLEfcr0+KN1i4sy+4e4hqckn9/4uJc/pnnLQqTkq+zAEht9 Lg85eKPIcHUS9SbcEU9MFUC1qYKA+Me087MkMe9qlbDU1B7dwHHkEh8mnVes/b/IutB6 xfaYH/XouUyXtA3n/z/EdHZutTnnYikZB7F+gK80L6i3/rEBQtM/k/ZTyIHsHHMufnDb YEnYXY+pUaRd3LF/U4GjIQBthBHlmitSvdhmzoIT4rEoJuCTLY7YMmDYUO7ksBthgQZp uaLg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=content-transfer-encoding:from:mime-version:subject:date:message-id :references:cc:in-reply-to:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=nSouztIGljQ7wgaG4sbHScReSAZxmraLrIcLGbzVNAk=; b=oFBOO6C/gjik4kH6iQF+pwyaMd+0ZMCy3E8wChtyQ0kPe5eFSU6BD/sB3pfH83vk0M nJjn7tVbnzTtC8SUTGi35JZpAnSqMvlkD+kdOmlLKSQIJ0hrig/IQ9CtG7YqE5/cQUYL T72mOSV2ADshYZNyvP1F6CwhszqiW8tIhZDNCF5ScvIfYRN8onTRDh0xO+b8jNQHmP02 HpvjjH2K5+ufEzSgl1LeSdTExNCpiTaADqmTqifcu0daj7+cfuONXq/YFboqf+BOkFk+ mDCTNs06/NE1523Mi5ZAkoxqfxWwGvPhhc4mibK4swMDUKQ2lrI9FDGYeKzoVaIVAsqY 9vRw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:content-transfer-encoding:from :mime-version:subject:date:message-id:references:cc:in-reply-to:to :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=nSouztIGljQ7wgaG4sbHScReSAZxmraLrIcLGbzVNAk=; b=OxMc5mkJh9/CP3K43PkvNM9yALZzyAEmkvY/KRF/5UnMBrS7yQndNasGJO61LPBThf s8XNJO1ETb8XCkDKJuoweL7qUfoYYduWo6ZzpNGXZW4cnTywFaCK88gLMYua7kIt3YWt tnhGl2di/7PiBHWOb1CkoVMHc7hqXDUu3Pu8Le28/xF4HclvGWK/4fbwlWpXtYohd916 5dBwBH1KpBegM++cy9xCBS1dZ89aPSvL4xdgArvE9gwKf62wC+ESTNbo4pRoVHdQVtyo Bm0IRhauoFCVdwarWBtaJSbWYim46KdhGZv4O67vRsTq6DwmlDasB4Ydna95TRJYeZXA cDPQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532xGibGIg82z2KeBCcZrKjXjnweL2KybJ4Zt516YLPxREbJxS2c 2VoCppD8jz6dOwtoo5P/PWo= X-Google-Smtp-Source: ABdhPJwrC+NEhYi1Ni+2/ahVhb38SuqcANYIeBv3KDv0qX1IirFm31ZMo1Y4wBBBJSdoJbIOZcuaVw== X-Received: by 2002:a7b:cb55:0:b0:38e:7dc6:40a3 with SMTP id v21-20020a7bcb55000000b0038e7dc640a3mr3000553wmj.82.1650021721788; Fri, 15 Apr 2022 04:22:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:2747:0:b0:381:80e8:be59 with SMTP id n68-20020a1c2747000000b0038180e8be59ls3790375wmn.1.gmail; Fri, 15 Apr 2022 04:22:00 -0700 (PDT) X-Received: by 2002:a05:600c:3b82:b0:38e:ccff:73ca with SMTP id n2-20020a05600c3b8200b0038eccff73camr2888723wms.77.1650021719987; Fri, 15 Apr 2022 04:21:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1650021719; cv=none; d=google.com; s=arc-20160816; b=BmCLCW0r+K+M0JTWYwYT2dLldwMku8zG64C1VcCTiYLyZSvkla/c8LyDktesehzWNW e4aAPXn4JvscB1Ixy7QRORVPvZ8VtsMb0wId5C9ayebi+xsYMdOVqvcIrv+Tn1e1JMxd B9tor0df7f+Hf8iUO6ZYXhnAQTyhI3rjVGKnLkrxnlXJjxZV4rkaHXwVOj/OMmcen0U1 K6fXTg1JFSJO718F7sDcrv5rKaa78mjLoucLxk2zCSMkPNHj3YMUtX6VAHdQ6zC4KyxT Oi9A+BJx0qJtnYuhRf60KRo17RDzTWqM/qeAeFDaaVTRH0q0CZy59Mv647qHMRMn3GZh O6DQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:cc:references:message-id:date:subject:mime-version :from:content-transfer-encoding:dkim-signature; bh=fHU2soHzo6jib35D0MicNqKcG6rppY2hbOauHHimdkg=; b=eChdJJV12ivtfPmUijMCAiZlMMgThgxWkbtuTOyo0lChtuBePyxqmqFw3ZSy+eClGp 6Ukvo4H8d5lp7FUlf2bcoQMcAlXlBWQQSn7RYLSIFF5gIWSqjR38RA3+1YMwFmYHEKMo obMW82pGYjlb+0npcmoXmApus4qPVHIa5dxQ/g6TwEsvKD0O4cRHs8gflH1U97/8Bekh 4ZxdvKbw2qOysFlQ+956KJrfaP95gMIUbChG8xQ0TGIQL/v2iWyABnyCcThdqRffOuka uHkxM6QlfcAbsWn6Chko7RcvDQYKanbHNUNJXdJdt2zoNmC747jTnN06ui04yAOlG81H 9rPw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=eRESr8ZL; spf=pass (google.com: domain of ondrej.rypacek@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=ondrej.rypacek@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32b.google.com (mail-wm1-x32b.google.com. [2a00:1450:4864:20::32b]) by gmr-mx.google.com with ESMTPS id u8-20020a056000038800b001f1f8f0f76csi73493wrf.3.2022.04.15.04.21.59 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 15 Apr 2022 04:21:59 -0700 (PDT) Received-SPF: pass (google.com: domain of ondrej.rypacek@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) client-ip=2a00:1450:4864:20::32b; Received: by mail-wm1-x32b.google.com with SMTP id m33-20020a05600c3b2100b0038ec0218103so4861539wms.3 for ; Fri, 15 Apr 2022 04:21:59 -0700 (PDT) X-Received: by 2002:a1c:f607:0:b0:381:1db:d767 with SMTP id w7-20020a1cf607000000b0038101dbd767mr2838689wmc.165.1650021719460; Fri, 15 Apr 2022 04:21:59 -0700 (PDT) Received: from smtpclient.apple ([2a01:4c8:487:5694:5a0:355a:7fe1:2879]) by smtp.gmail.com with ESMTPSA id f1-20020a1c6a01000000b0038c9f6a3634sm7943184wmc.7.2022.04.15.04.21.58 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 15 Apr 2022 04:21:58 -0700 (PDT) Content-Type: multipart/alternative; boundary=Apple-Mail-ABD9903C-D4C6-4C47-8EEE-D03CA339389A Content-Transfer-Encoding: 7bit From: Ondrej Rypacek Mime-Version: 1.0 (1.0) Subject: Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Date: Fri, 15 Apr 2022 12:21:57 +0100 Message-Id: <305B4B55-F94D-4BFF-BC80-DF8A92172885@gmail.com> References: <776cef63-67d8-4413-9cf6-c005e548c386n@googlegroups.com> Cc: Homotopy Type Theory In-Reply-To: <776cef63-67d8-4413-9cf6-c005e548c386n@googlegroups.com> To: Josh Chen X-Mailer: iPhone Mail (19D52) X-Original-Sender: ondrej.rypacek@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=eRESr8ZL; spf=pass (google.com: domain of ondrej.rypacek@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=ondrej.rypacek@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: , --Apple-Mail-ABD9903C-D4C6-4C47-8EEE-D03CA339389A Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear all, as an outsider, so someone with no fear of carreer repercussions, and also = someone who grew up in communist Czechoslovakia, let me say this: this is v= ery reminiscent of the communist profiling of people=E2=80=99s =E2=80=9Ccor= rect ideological attitudes=E2=80=9D, when only the vetted people were allow= ed to publish and work in their field. I fail to see the connection between HOTT and gender issues, important as i= t may be to some. In the end you end up with people who are meidocre accade= micaly but ideologically agile. Have a good day, Ondrej=20 > On 15 Apr 2022, at 10:29, Josh Chen wrote: >=20 > =EF=BB=BF > I find the situation unfortunate and was also very much looking forward t= o learning more from Mike, >=20 > But as someone who followed the events that Andrej has described from the= start, with sadness I support the decision by the HoTTEST organizers to no= t hold the lectures immediately thereafter under the auspices of a Distingu= ished series. >=20 > If nothing else, I feel it would have been premature that soon, and would= have worked against the goal of welcoming people of all gender presentatio= ns and identities. I am not myself trans and can thus easily afford to "tol= erate" the public declaration of positions that lead to worse societal outc= omes for them. But this is not the case for the significant number of trans= people in, and adjacent to, the HoTT community, some of whom have to activ= ely hide this part of themselves on pain of e.g. family violence. We should= think about such things when considering using hot-button phrases like "po= litical correctness" and "cancel culture". >=20 > I certainly look forward to hearing about Mike's (and Thorsten's and Ambr= us's) ideas in another format or on another occasion. >=20 > With respect and kind regards, > Josh >=20 >=20 >> On Friday, April 15, 2022 at 4:00:12 AM UTC+1 axh...@gmail.com wrote: >> I would love to hear Mike's lectures.=20 >>=20 >> All the best wishes,=20 >>=20 >> Alexander=20 >>=20 >> > On Apr 14, 2022, at 13:23, Nicolas Alexander Schmidt wrote:=20 >> >=20 >> > Dear Chris,=20 >> >=20 >> >=20 >> > with great interest I saw the advertisement for Mike's upcoming talk. = When I saw that the announcement had spawned a proper thread, I of course a= ssumed it was because of the interesting mathematical content.=20 >> >=20 >> > I was greatly disappointed to learn that the reason was not mathematic= s at all.=20 >> >=20 >> > Mathematics, like any endeavour, can only thrive when it is a meritocr= acy. You don't have to like someone or agree with his political views to ap= preciate his ideas. And Mike is one of the best people in the field, if not= the best. So, why are you trying to cancel him, Chris? Are you trying to a= dvance your own career?=20 >> >=20 >> > By cancelling him, by preventing him from disseminating his ideas, you= are damaging the whole field. Don't pretend that you're making a "difficul= t decision" when you are acting selfishly and reprehensibly.=20 >> >=20 >> >=20 >> > Best,=20 >> >=20 >> > Nicolas=20 >> >=20 >> >> The organizers of the HoTT Electronic Seminar Talks are committed to= =20 >> >> the diversity and growth of homotopy type theory, and want everybody= =20 >> >> to feel comfortable and welcome in our community.=20 >> >>=20 >> >> We believe the speaker=E2=80=99s recent statements in the context of = the HoTT=20 >> >> Book stand in opposition to these values, and have made the difficult= =20 >> >> decision not to hold the upcoming HoTTEST Distinguished Lecture=20 >> >> Series.=20 >> >>=20 >> >> Carlo Angiuli=20 >> >> Dan Christensen=20 >> >> Chris Kapulkin=20 >> >>=20 >> >> On Mon, Apr 11, 2022 at 9:32 AM Chris Kapulkin w= rote:=20 >> >>> We are delighted to announce the inaugural HoTTEST Distinguished=20 >> >>> Lecture Series to be given by Mike Shulman (University of San Diego)= .=20 >> >>> The series consists of three lectures which will take place on April= =20 >> >>> 14, 21, and 28 at 11:30 AM Eastern time. The Eastern time zone is no= w=20 >> >>> observing daylight saving time, making it UTC-04:00.=20 >> >>>=20 >> >>> Each lecture will be one-hour long and will be followed by a 30-minu= te=20 >> >>> discussion. The title and abstract are below.=20 >> >>>=20 >> >>> The Zoom link is=20 >> >>>=20 >> >>> https://zoom.us/j/994874377=20 >> >>>=20 >> >>> Further information, including our Google Calendar and Youtube=20 >> >>> channel, is available at=20 >> >>>=20 >> >>> http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html=20 >> >>>=20 >> >>> We are looking forward to seeing many of you there!=20 >> >>>=20 >> >>> Best wishes,=20 >> >>> Carlo Angiuli=20 >> >>> Dan Christensen=20 >> >>> Chris Kapulkin=20 >> >>>=20 >> >>> *=20 >> >>>=20 >> >>> Mike Shulman=20 >> >>> University of San Diego=20 >> >>>=20 >> >>> Towards Third-Generation HOTT=20 >> >>>=20 >> >>> In Book HoTT, identity is defined uniformly by the principle of=20 >> >>> "indiscernibility of identicals". This automatically gives rise to= =20 >> >>> higher structure; but many desired equalities are not definitional,= =20 >> >>> and univalence must be asserted by a non-computational axiom. Cubica= l=20 >> >>> type theories also define identity uniformly, but using paths instea= d.=20 >> >>> This makes more equalities definitional, and enables a form of=20 >> >>> univalence that computes; but requires inserting all the higher=20 >> >>> structure by hand with Kan operations.=20 >> >>>=20 >> >>> I will present work in progress towards a third kind of homotopy typ= e=20 >> >>> theory, which we call Higher Observational Type Theory (HOTT). In th= is=20 >> >>> system, identity is not defined uniformly across all types, but=20 >> >>> recursively for each type former: identifications of pairs are pairs= =20 >> >>> of identifications, identifications of functions are pointwise=20 >> >>> identifications, and so on. Univalence is then just the instance of= =20 >> >>> this principle for the universe. The resulting theory has many usefu= l=20 >> >>> definitional equalities like cubical type theories, but also gives= =20 >> >>> rise to higher structure automatically like Book HoTT. Also like Boo= k=20 >> >>> HoTT, it can be interpreted in a class of model categories that=20 >> >>> suffice to present all Grothendieck-Lurie (=E2=88=9E,1)-toposes; and= we have=20 >> >>> high hopes that, like cubical type theories, some version of it will= =20 >> >>> satisfy canonicity and normalization.=20 >> >>>=20 >> >>> This is joint work with Thorsten Altenkirch and Ambrus Kaposi.=20 >> >=20 >> > --=20 >> > You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group.=20 >> > To unsubscribe from this group and stop receiving emails from it, send= an email to HomotopyTypeThe...@googlegroups.com.=20 >> > To view this discussion on the web visit https://groups.google.com/d/m= sgid/HomotopyTypeTheory/876f6e58-211c-4824-e938-4b915e18d859%40fromzerotoin= finity.xyz.=20 >>=20 >=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/776cef63-67d8-4413-9cf6-c005e548c386n%40googlegroups.c= om. --=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/305B4B55-F94D-4BFF-BC80-DF8A92172885%40gmail.com. --Apple-Mail-ABD9903C-D4C6-4C47-8EEE-D03CA339389A Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

as an outsider,= so someone with no fear of carreer repercussions, and also someone who gre= w up in communist Czechoslovakia, let me say this: this is very reminiscent= of the communist profiling of people=E2=80=99s =E2=80=9Ccorrect ideologica= l attitudes=E2=80=9D, when only the vetted people were allowed to publish a= nd work in their field.

I = fail to see the connection between HOTT and gender issues, important as it = may be to some. In the end you end up with people who are meidocre accademi= caly but ideologically agile.

Have a good day,
Ondrej 



On 15 Apr 2022, at 10:29, Josh Chen <jaycech3n@gmail.com>= wrote:

=EF=BB=BF
I find the situation unfortunate and was also very much loo= king forward to learning more from Mike,

But as someone who followed the events that Andrej has described from the=20 start, with sadness I support the decision by the HoTTEST organizers to=20 not hold the lectures immediately thereafter under the auspices of a=20 Distinguished series.

If nothing else, I feel=20 it would have been premature that soon, and would have worked against=20 the goal of welcoming people of all gender presentations and identities. I am not myself trans and can thus easily afford to "tolerate" the=20 public declaration of positions that lead to worse societal outcomes for them. But this is not the case for the significant number of trans=20 people in, and adjacent to, the HoTT community, some of whom have to=20 actively hide this part of themselves on pain of e.g. family violence.=20 We should think about such things when considering using hot-button=20 phrases like "political correctness" and "cancel culture".

I certainly look forward to hearing about Mike's (and Thorsten's a= nd Ambrus's) ideas in another format or on another occasion.

=
With respect and kind regards,
Josh


On Friday, Apr= il 15, 2022 at 4:00:12 AM UTC+1 axh...@gmail.com wrote:
I would love to hear Mike's lectu= res.

All the best wishes,

Alexander

> On Apr 14, 2022, at 13:23, Nicolas Alexander Schmidt <ze...@fromzerotoinfinity.xyz<= /a>> wrote:
>=20
> Dear Chris,
>=20
>=20
> with great interest I saw the advertisement for Mike's upcoming ta= lk. When I saw that the announcement had spawned a proper thread, I of cour= se assumed it was because of the interesting mathematical content.
>=20
> I was greatly disappointed to learn that the reason was not mathem= atics at all.
>=20
> Mathematics, like any endeavour, can only thrive when it is a meri= tocracy. You don't have to like someone or agree with his political views t= o appreciate his ideas. And Mike is one of the best people in the field, if= not the best. So, why are you trying to cancel him, Chris? Are you trying = to advance your own career?
>=20
> By cancelling him, by preventing him from disseminating his ideas,= you are damaging the whole field. Don't pretend that you're making a "diff= icult decision" when you are acting selfishly and reprehensibly.
>=20
>=20
> Best,
>=20
> Nicolas
>=20
>> The organizers of the HoTT Electronic Seminar Talks are commit= ted to
>> the diversity and growth of homotopy type theory, and want eve= rybody
>> to feel comfortable and welcome in our community.
>>=20
>> We believe the speaker=E2=80=99s recent statements in the cont= ext of the HoTT
>> Book stand in opposition to these values, and have made the di= fficult
>> decision not to hold the upcoming HoTTEST Distinguished Lectur= e
>> Series.
>>=20
>> Carlo Angiuli
>> Dan Christensen
>> Chris Kapulkin
>>=20
>> On Mon, Apr 11, 2022 at 9:32 AM Chris Kapulkin <k.kap...@gmail.com> wrote:
>>> We are delighted to announce the inaugural HoTTEST Disting= uished
>>> Lecture Series to be given by Mike Shulman (University of = San Diego).
>>> The series consists of three lectures which will take plac= e 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/9948743= 77
>>>=20
>>> Further information, including our Google Calendar and You= tube
>>> channel, is available at
>>>=20
>>> http://uwo.ca/math/faculty/kapulkin/semi= nars/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 princip= le of
>>> "indiscernibility of identicals". This automatically gives= rise to
>>> higher structure; but many desired equalities are not defi= nitional,
>>> and univalence must be asserted by a non-computational axi= om. Cubical
>>> type theories also define identity uniformly, but using pa= ths instead.
>>> This makes more equalities definitional, and enables a for= m of
>>> univalence that computes; but requires inserting all the h= igher
>>> structure by hand with Kan operations.
>>>=20
>>> I will present work in progress towards a third kind of ho= motopy type
>>> theory, which we call Higher Observational Type Theory (HO= TT). 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 point= wise
>>> identifications, and so on. Univalence is then just the in= stance of
>>> this principle for the universe. The resulting theory has = many useful
>>> definitional equalities like cubical type theories, but al= so gives
>>> rise to higher structure automatically like Book HoTT. Als= o like Book
>>> HoTT, it can be interpreted in a class of model categories= that
>>> suffice to present all Grothendieck-Lurie (=E2=88=9E,1)-to= poses; 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 Kap= osi.
>=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 Homot= opyTypeThe...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/Homotopy= TypeTheory/876f6e58-211c-4824-e938-4b915e18d859%40fromzerotoinfinity.xyz.

--
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.goog= le.com/d/msgid/HomotopyTypeTheory/776cef63-67d8-4413-9cf6-c005e548c386n%40g= ooglegroups.com.

--
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/msg= id/HomotopyTypeTheory/305B4B55-F94D-4BFF-BC80-DF8A92172885%40gmail.com.=
--Apple-Mail-ABD9903C-D4C6-4C47-8EEE-D03CA339389A--