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 very reminiscent of the communist profiling of people’s “correct ideological attitudes”, when only the vetted people were allowed to publish and 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 accademicaly but ideologically agile. Have a good day, Ondrej > On 15 Apr 2022, at 10:29, Josh Chen wrote: > >  > I find the situation unfortunate and was also very much looking forward to learning more from Mike, > > 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 not hold the lectures immediately thereafter under the auspices of a Distinguished series. > > 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 presentations and identities. I am not myself trans and can thus easily afford to "tolerate" the public declaration of positions that lead to worse societal outcomes 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 actively 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 "political correctness" and "cancel culture". > > I certainly look forward to hearing about Mike's (and Thorsten's and 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 wrote: >> > >> > Dear Chris, >> > >> > >> > 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 assumed it was because of the interesting mathematical content. >> > >> > I was greatly disappointed to learn that the reason was not mathematics at all. >> > >> > 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 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? >> > >> > 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 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’s 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 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. >> >>> >> >>> 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 (∞,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. >> > >> > -- >> > 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/HomotopyTypeTheory/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 email 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. -- 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/305B4B55-F94D-4BFF-BC80-DF8A92172885%40gmail.com.