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 7409 invoked from network); 15 Apr 2022 09:29:44 -0000 Received: from mail-yw1-x1139.google.com (2607:f8b0:4864:20::1139) by inbox.vuxu.org with ESMTPUTF8; 15 Apr 2022 09:29:44 -0000 Received: by mail-yw1-x1139.google.com with SMTP id 00721157ae682-2e61c5a0eb7sf62282897b3.22 for ; Fri, 15 Apr 2022 02:29:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=A/Iyln2AqkmJDzOS4m0BSGBOY5j1REb9CqoPow1gjYk=; b=f6sEd88I8AtDzfRWOwfppx5fJsmJmeEIHL6n0qkGQXI6p4C1LuYy2qCp2NFfmNmZhE wVq6IOJ2C26eaz2QnobLFr9kAEAf9UuJk7IioyjeVrYHfiqoyDaeqvP1RHs6oU2DgGyY PNjf4yvADLfrPM4rukCbvZ77h8EBkYsjo8kY9oyQGpR4VTUexzvSENdDOYJ8tBNilboV ksRBKysXBr3dz6j0xHdX/0JtCu2slXL5o3h52RvJ8giQhZXaVHzFUumVw5F7Pobf4gDG dyiMZlz1DzmMDyHz6nfZz4zCx00W9Ql/ELeN6NxwW5LGwz51iYrighfym0a+dzI7cMhR 0NaQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-subscribe:list-unsubscribe; bh=A/Iyln2AqkmJDzOS4m0BSGBOY5j1REb9CqoPow1gjYk=; b=PFegIRnA5f+wDhBj2nUraTws0QwKEZTJ1F3L6Y3Rm0LEiYi+bOpatmHOBBBqGSAoKg IgVzmYJmsqMSJ9L6pNYh33ptXZXQQD1hZ3hLTMHhUjo5o8IIJdip/4Ev5VPhBjiWCa90 cHQCUhdia/q5fDjWZrukXl3w31Xb0/6IuiS4vDd0/1n+POTYRx849S6RYhECe4WOOfL0 QRcXvY0A+XAGIFAWBCduDKMkC1m7KRjBC7LQUcx0oLV3VAvg8dtXXqNkRstVPD5piGUz zZLGTGkPuwF58u9YL7EaYVc5leftwzb1J07et9dOp80Hz/c1youRzx1+uf2YgJ1Ebn5j HB9w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=A/Iyln2AqkmJDzOS4m0BSGBOY5j1REb9CqoPow1gjYk=; b=4SX9RyiYLjtwBqG3/+KGvHTRRfxcrgi27WrfH0bSaPk93OMbi2K0SNVQAejLFtKaDv o1K+gWQFdvo+Xq7N7m6KYfsCPGnI3J+W7NS5m/VRgTjSOQNKqnBPnMLOwODlwD0wwLNF +gZCLy8WxnCqcnYAG+vfCLmvppGd6GuPqMz3ABjVPsPaBgGSKeLzqIk74BKLc9lle4Yl a7HnbZmvo6ktLNiP89x/F6YfDCY9/eY/B8Ro0nO0V1Mc2E1L0fC+8Ag7vZ8QVdKUtjX7 7IaQ4uQdHj/8Giy34wBLn4f4Stir0isO6B0yJKmqkQH/ym4KPMYggbR3kH/oWCTc3Jzz M/9g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532Jv5c+NhKvGNj8KqS4QAGVz1pkxFu3puXThRbmq+ItSjrGgEtt kGdUhBYuW6YBLcCeUlIlCiA= X-Google-Smtp-Source: ABdhPJwNP+jjfl8p4g67LHGXt1FHiJ1N9YoT/0Wsu+DaDLM90Ra1XsKRmk0LU3HEH5v2lEq/MUsrgA== X-Received: by 2002:a81:604:0:b0:2e6:6b45:4812 with SMTP id 4-20020a810604000000b002e66b454812mr5294207ywg.266.1650014983060; Fri, 15 Apr 2022 02:29:43 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:5e09:0:b0:641:5127:8328 with SMTP id s9-20020a255e09000000b0064151278328ls5254206ybb.10.gmail; Fri, 15 Apr 2022 02:29:42 -0700 (PDT) X-Received: by 2002:a25:8702:0:b0:641:39fa:f44c with SMTP id a2-20020a258702000000b0064139faf44cmr4715137ybl.460.1650014981921; Fri, 15 Apr 2022 02:29:41 -0700 (PDT) Date: Fri, 15 Apr 2022 02:29:41 -0700 (PDT) From: Josh Chen To: Homotopy Type Theory Message-Id: <776cef63-67d8-4413-9cf6-c005e548c386n@googlegroups.com> In-Reply-To: <6A66F50E-FAF2-4C31-ABA9-835ED4FDE345@gmail.com> References: <876f6e58-211c-4824-e938-4b915e18d859@fromzerotoinfinity.xyz> <6A66F50E-FAF2-4C31-ABA9-835ED4FDE345@gmail.com> Subject: Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_792_1411319242.1650014981154" X-Original-Sender: jaycech3n@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: , ------=_Part_792_1411319242.1650014981154 Content-Type: multipart/alternative; boundary="----=_Part_793_79555805.1650014981154" ------=_Part_793_79555805.1650014981154 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I find the situation unfortunate and was also very much looking forward to= =20 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 not= =20 hold the lectures immediately thereafter under the auspices of a=20 Distinguished series. If nothing else, I feel it would have been premature that soon, and would= =20 have worked against the goal of welcoming people of all gender=20 presentations and identities. I am not myself trans and can thus easily=20 afford to "tolerate" the public declaration of positions that lead to worse= =20 societal outcomes for them. But this is not the case for the significant=20 number of trans people in, and adjacent to, the HoTT community, some of=20 whom have to actively hide this part of themselves on pain of e.g. family= =20 violence. We should think about such things when considering using=20 hot-button phrases like "political correctness" and "cancel culture". I certainly look forward to hearing about Mike's (and Thorsten's and=20 Ambrus's) ideas in another format or on another occasion. With respect and kind regards, Josh On Friday, April 15, 2022 at 4:00:12 AM UTC+1 axh...@gmail.com wrote: > I would love to hear Mike's lectures. > > All the best wishes, > > Alexander > > > On Apr 14, 2022, at 13:23, Nicolas Alexander Schmidt < > ze...@fromzerotoinfinity.xyz> wrote: > >=20 > > Dear Chris, > >=20 > >=20 > > 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 course= =20 > assumed it was because of the interesting mathematical content. > >=20 > > I was greatly disappointed to learn that the reason was not mathematics= =20 > at all. > >=20 > > 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? > >=20 > > 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 "difficu= lt=20 > decision" 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 t= he 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 =20 > wrote: > >>> 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-minut= e > >>> 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 thi= s > >>> 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=20 > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeThe...@googlegroups.com. > > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/876f6e58-211c-4824-e= 938-4b915e18d859%40fromzerotoinfinity.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/776cef63-67d8-4413-9cf6-c005e548c386n%40googlegroups.com= . ------=_Part_793_79555805.1650014981154 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I find the situation unfortunate and was also very much looking forwar= d 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 = lectures.

All the best wishes,

Alexander

> On Apr 14, 2022, at 13:23, Nicolas Alexander Schmidt <ze...@fromzerotoinfinity.xyz> wrot= e:
>=20
> Dear Chris,
>=20
>=20
> with great interest I saw the advertisement for Mike's upcomin= g talk. When I saw that the announcement had spawned a proper thread, I of = course 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 vie= ws to 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 try= ing 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 "difficult decision" when you are acting selfishly and reprehe= nsibly.
>=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 automatic= ally 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 HomotopyTypeThe= ...@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 &= 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.c= om/d/msgid/HomotopyTypeTheory/776cef63-67d8-4413-9cf6-c005e548c386n%40googl= egroups.com.
------=_Part_793_79555805.1650014981154-- ------=_Part_792_1411319242.1650014981154--