M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series

1,585 views
Skip to first unread message

Chris Kapulkin

unread,
Apr 11, 2022, 9:33:00 AM4/11/22
to HoTT Electronic Seminar Talks, Homotopy Type Theory, categ...@mta.ca
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.

Chris Kapulkin

unread,
Apr 13, 2022, 9:28:42 PM4/13/22
to HoTT Electronic Seminar Talks, Homotopy Type Theory, categ...@mta.ca
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

Thorsten Altenkirch

unread,
Apr 14, 2022, 4:32:59 AM4/14/22
to Chris Kapulkin, HoTT Electronic Seminar Talks, Homotopy Type Theory, categ...@mta.ca

Hi,

 

Was this necessary? I don’t agree with Mike’s views on transgender issues but this has nothing to do with the topic of the seminar. Maybe he should have refrained on expressing them in the context of the HoTT book but maybe it is not good if people can’t say what they think even if we don’t agree with it.

 

In the end cancelling the seminar is water on the mills of certain right wing people who will see this as yet another example of “cancel culture”. Maybe you felt that you needed to cancel it to avoid it to get hijacked to discuss topics which have nothing to do with the topic but then you should have said this.

 

Cheers,

Thorsten

--
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/CAEXhy3Pjt4%3Dwi5ikinGTqkKXyQKQ6iWOCtyTjz%3DBc1zufLz-AQ%40mail.gmail.com.


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.



Urs Schreiber

unread,
Apr 14, 2022, 5:25:22 AM4/14/22
to Chris Kapulkin, HoTT Electronic Seminar Talks, Homotopy Type Theory, categories
On Thu, Apr 14, 2022 at 5:28 AM Chris Kapulkin <k.kap...@gmail.com> wrote:

> We believe the speaker’s recent statements in the context of the HoTT
> Book stand in opposition to these values

Scrolling up this thread for context, one gathers you must be
referring to this statement:

"In Book HoTT, identity is defined uniformly [...] many desired
equalities are not definitional".

While possibly scandalous, I am tolerant and was looking forward to
seeing the arguments,
if not for moral but for intellectual edification.

Is there a draft or preprint available of the announced work by
Altenkirch, Shulman & Kaposi?
It sounds intriguing.

Thomas Streicher

unread,
Apr 14, 2022, 6:42:44 AM4/14/22
to Chris Kapulkin, HoTT Electronic Seminar Talks, Homotopy Type Theory, categ...@mta.ca
> 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.

Thank you for this reveiling discussion. Has nicely enforced all the
prejudices(?) I have against PC attitude.

I am attending international meetings since the mid 80s and never
observed any discrimination. This seems to be a more recent phenomenon
since civilized liberal communicatio has been replaced by moralistic terror.

A benevolent interpretation is that you want to avoid further hassle which I
can understand. But I am afraid some people mean seriously what they say...

In my eyes it is absurd to prevent people from giving a scientific talk
because of a "grammatical mistake".

Trying to enforce absolute virtue leads to absolute terror. Have
considered this a house-and-garden wisdom taught by history since the
Jacobinians.
Well, no blood has flown yet in the HoTT community :-) but the
increasing animosity caused by (mis?)use of the Internet has damaged
our societies sufficiently much.

No need to blame me as conservative or reactionary. In THIS context I
would take it as a compliment. And I will not react.

Leaving aside this parodistic epsiode I am confident that Mike will
get the opportunity to present the intriguing points sketched in his
abstract within another format!

Thomas





Andrej Bauer

unread,
Apr 14, 2022, 7:49:15 AM4/14/22
to HoTT Electronic Seminar Talks, Homotopy Type Theory, categ...@mta.ca
The organizers of the HoTTest seminar did not refer explicitly to the events that prompted them to take their decision, which leaves many people surprised and in the dark. I worry that it may also lead to unfounded speculation and uninformed opinions. As one of the administrators and a HoTT book author I led an effort to bring to conclusion the episode that the HoTTest seminar organizers implicitly referred to. Please allow me then to give a short but incomplete account of the events of the past days as I see it.

A while ago, there was a HoTT book pull request #1101 asking that "he or she" be replaced with "they", for reasons of inclusivity. The ensuing discussion took on a wider context. Mike Shulman and Dan Grayson expressed views which the other participants strongly opposed and found offensive. Many members of the HoTT community, including authors of the HoTT book, readers, and students, spoke out against Mike's statements and presented reasons for inclusivity. Some described how the issue affected them personally, which I am sure was not easy to do. Overall the discussion was civilized, even though emotions ran high.

The administrators of the HoTT book repository, one of whom is Mike Shulman, unanimously decided to implement the proposed change, as it had very clear support. In addition, Mike Shulman acknowledged that the pull request was not an appropriate place for political discussions, and apologized for derailing the conversation in that direction. He expressed regret that his attempts to explain his views hurt people's feelings. He stated that he meant no harm to anyone.

At present there is a related issue open, issue #1111, in which a Code of conduct is being discussed, with the purpose of making sure that such incidents do not happen in the future, and that the community can continue to be welcoming to everyone.

I urge anyone who intends to express an opinion to not base it solely on what I have written here.

With kind regards,

Andrej




Martín Hötzel Escardó

unread,
Apr 14, 2022, 11:49:10 AM4/14/22
to Homotopy Type Theory
I am not happy at all with what Mike said in the above pull request discussion, and I said so there, but at the same time I think that cancelling his talk was the wrong thing to do.

Everybody should move on positively after the resolution that Andrej discussed above, and I don't consider cancelling his talk to be a positive move.

I am by no means excusing Mike from what he did - this is something he should work on to resolve himself.

What I am saying is that cancelling somebody who has apologized publicly is not contributing to reinstate the welcoming atmosphere we've had in this community for a long time here.

Martin

Joyal, André

unread,
Apr 14, 2022, 11:49:12 AM4/14/22
to Chris Kapulkin, HoTT Electronic Seminar Talks, Homotopy Type Theory, categ...@mta.ca
To the organisers of the HoTTEST Distinguished Lecture Series:
Carlo Angiuli,
Dan Christensen
Chris Kapulkin


I am very disappointed you have cancelled the lectures by Mike Shulman.
I respectfully ask you to reconsider your decision, irrespective of  Mike's opinion.

Best wishes,
André Joyal

De : homotopyt...@googlegroups.com <homotopyt...@googlegroups.com> de la part de Chris Kapulkin <k.kap...@gmail.com>
Envoyé : 11 avril 2022 09:32
À : HoTT Electronic Seminar Talks <hott-electroni...@googlegroups.com>; Homotopy Type Theory <homotopyt...@googlegroups.com>; categ...@mta.ca <categ...@mta.ca>
Objet : [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
 
--
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.

Nicolas Alexander Schmidt

unread,
Apr 14, 2022, 4:23:45 PM4/14/22
to HomotopyT...@googlegroups.com
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

Alexander Kurz

unread,
Apr 14, 2022, 11:00:12 PM4/14/22
to HomotopyT...@googlegroups.com
I would love to hear Mike's lectures.

All the best wishes,

Alexander
> --
> 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.

Josh Chen

unread,
Apr 15, 2022, 5:29:41 AM4/15/22
to Homotopy Type Theory
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

Ondrej Rypacek

unread,
Apr 15, 2022, 7:22:01 AM4/15/22
to Josh Chen, Homotopy Type Theory
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 <jayc...@gmail.com> wrote:



Martín Hötzel Escardó

unread,
Apr 15, 2022, 8:01:12 AM4/15/22
to Homotopy Type Theory
Unfortunately, this is a lose-lose situation. But I find Josh's argument below much more persuasive than mine above, and I agree with every single word. Martin

David

unread,
Apr 23, 2022, 10:47:14 AM4/23/22
to Homotopy Type Theory
I literally cannot find anything wrong or upsetting or offensive in Mike's comments on the github.  He got dislike-bombed for talking about a matter of style, and he got an avalanche of criticism for disagreeing with the latest newly-minted dogma of inclusivity.  People are in this very thread condemning him for his 'views'.  His views of what? Writing style? Grammar?  By disagreeing with the (constantly changing, mind) new dogma, he had to endure a struggle session, and still, afterwards, he's being treated as a pariah and having his talks cancelled?

Mike is one of the most important people in the field (top 3 for sure).  He's demonstrated his bona fides (mathematical and otherwise) time and time again.  He's a good guy, and you guys have cast the most outrageous aspersions against him, as if he were some kind of bigot.

Come on.  Get real.  

David 

Andreas Nuyts

unread,
Apr 23, 2022, 3:36:55 PM4/23/22
to Homotopy Type Theory
Dear all,

Without implying my agreement with Davids entire mail, I do think the following argument:

constantly changing, mind

is rather important. I hope we all agree that an attitude of social inclusion is of the utmost importance. However, it is undeniable that insights as to what it entails to be socially inclusive are rapidly evolving (and understandably so: the cultures that we all grew up in are the same ones that produce the phenomena of social exclusion that we should seek to avoid). Even ignoring for a moment the possibility that this evolution may give rise to legitimate differences of opinion (a possibility which should not be ignored!), it is completely unreasonable to expect every single person to be on the vanguard of this evolution in every single aspect of it at every single point in time.
Calling someone who exhibits exclusionary behaviour a bigot, suggests an inherent and permanent corruption of their personality. Most often, I think, we should instead explain exclusionary behaviour either from unawareness of some or all aspects of the problem, or from a lack of courage needed to rise up against the mechanisms of exclusion.

If a person in a position of power or privilege should exhibit exclusionary behaviour, then this is a problem that requires attention. Discarding the person altogether is a simple but also wasteful, preposterous and unjust solution. Moreover, I would rather see people with exclusionary ideas (such as probably all of us in at least some way) speak up and lay out their arguments so that these can be refuted in a serene discussion, than I would see them stay silent and act according to their ideas for perhaps an entire lifetime. In my view, installing a culture of fear and self-censorship is counterproductive.

That being said, I do think we all have the responsibility to adopt a proactive attitude in informing ourselves about phenomena of social in/exclusion (and other societal problems that we may have an impact on). In particular, we should be willing to learn when called out (and willing to explain when calling out) on our behaviour.

Best regards,
Andreas Nuyts
--
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.

David

unread,
Apr 25, 2022, 5:36:13 AM4/25/22
to Homotopy Type Theory
I don't know what you mean that 'an attitude of social inclusion is of the utmost importance'.  In terms of priorities, it's certainly down in the double digits for me (and likely for the rest of you too, if you're being honest with yourself), not to say I don't find it important at all, just that I think 'utmost' is overegging the custard.  Also, I don't think that anything that Mike said could possibly be construed as him having an attitude of exclusion.  He shows up in a thread, gives his two cents, and then is put upon by people making demands that he speak in a certain way.  I have to ask: On what authority do these people rely to make such demands?  If it's not on the grounds of authority, the burden is on them to persuade.

What happened to Mike is a clear-cut case of academic bullying.  People who can't clearly stick up for him and want to hem and haw and sit on the fence are absolute cowards, and the people condemning him outright are not living in the real world.  

Best,

David

Josh Chen

unread,
Apr 25, 2022, 12:23:56 PM4/25/22
to Homotopy Type Theory
Dear David,

It would be quite nice for those of us who are using our real, full names, and largely being civil in sharing our opinions, to know which of the multiple Davids in this area we are addressing when we have to respond to factual inaccuracies and charges of cowardice, please? I cannot deduce this from your anonymous email address.

> People are in this very thread condemning him for his 'views'...you guys have cast the most outrageous aspersions against him, as if he were some kind of bigot.

You might be mixing up the comments here and those on the GitHub PR. I don't see anyone here (myself included) condemning Mike or calling him a bigot, even though his choice of words in the PR was very regrettable in drawing the analogy between trans/non-binary people and "abnormalities", which is exactly the kind of thing that reinforces the prejudice that gets queer people harassed, assaulted, and killed (https://www.reuters.com/article/lgbt-crime-rights-idUSL8N2804FQ, https://www.reuters.com/article/us-new-zealand-lgbt-health-idUSKBN1W9057, https://vawnet.org/sc/serving-trans-and-non-binary-survivors-domestic-and-sexual-violence/violence-against-trans-and; I could go on).

This will also be my last response on this thread, as I don't believe online debate with an anonymous, antagonistic interlocutor is productive.

David

unread,
Apr 25, 2022, 3:25:21 PM4/25/22
to Homotopy Type Theory
After seeing what you did here did to Mike, no chance.  When you guys decide to stop retaliating against people for having a difference of opinion, I will be happy to unmask myself.  

I don't understand why you're bringing up articles about hate crimes.  We're talking about an objection to using a plural (or arguably singular indefinite) pronoun for a definite subject.  It sounds weird.  It's confusing to read.  Mike's talk was cancelled over this.  He didn't commit, encourage, support, or have anything positive to say about hate crimes.  Moreover, I know that he doesn't do any of the above, and you do too.  The reason why you're angry is because Mike decided not to immediately bow to your demands about how to speak.  It reminds me very much of the current situation in Russia, where you can be sanctioned for using particular language (special mathematical operation?).  

You should really check your authoritarian impulses and calm down.

Best,

David

Josh Chen

unread,
Apr 25, 2022, 9:18:59 PM4/25/22
to Homotopy Type Theory
> I don't understand why you're bringing up articles about hate crimes.
> The reason why you're angry...

I'm afraid I have to break my previous promise in order to correct the record: in case there is any doubt, I am not angry with Mike, indeed I look forward to his upcoming talk.

I also do not appreciate the arrogance of an online anonymous who might not even be a part of this community, and who is clearly not thinking level-headedly enough to read and comprehend my previous sentences---much less the content of this thread---to presume to call others here absolute cowards, or to tell me what I am feeling.

In case it's not clear and since this is on the public record, let me reiterate for the final time my point, almost verbatim from my last message: "drawing the analogy between trans/non-binary people and "abnormalities" is exactly the kind of thing that reinforces the prejudice that gets them harassed, assaulted, and killed." I am simply pointing out that there are real people in our community who have an objectively worse time in society because of the way they were born, and we should be mindful that we do not perpetuate the stigma of "abnormality" that results in this.

With your great free speech comes great responsibility, which is unfortunately not a lesson learned by many "free speech absolutists".

David

unread,
Apr 25, 2022, 10:04:20 PM4/25/22
to Homotopy Type Theory
Of course Mike didn't draw an analogy between trans/nonbinary people and 'abnormalities'.  In fact, his interlocutor suggested that _sex_ (and specifically not gender) was a spectrum.  Mike correctly noted that being intersex is medically considered to be an abnormality, with varying degrees of disability resulting (depending on which extra chromosomes appear in the genome).  You got so caught up in your great moralistic crusade over this that you didn't even pay attention to what he said.

Your crusade has converted an abstract, potential, and linguistic harm to people in society at large to an actual harm to Mike and also to everyone who cares what he has to say.  Moreover, it's damaged the community by splitting people into camps (either you're for trans/nonbinary murder or you're opposed to it, I guess?).  

And for the record, I'm not directly part of the HoTT community, but I'm immediately adjacent to it mathematically and have attended many HoTT-themed events (and I'm familiar specifically with the problem that Mike's new work is trying to solve).  Since I don't want to reveal who I am, I won't say too much more than this: I know Mike pretty well; I have met him in person; and I think he's a stand-up guy.  And you're sitting here spreading innuendo about him.  I think that's BS, so I'm standing up for him.  

Best,

David

PS You're not fooling me into revealing who I am., because 'taking responsibility' here means subjecting myself to retaliation by small-minded bigots like yourself.  Also, I don't know where this 'free speech absolutist' stuff is coming from, but maybe it's better if you move to an authoritarian state where people are forced to respect one another obsequiously and follow the party line.  Again, you should check your authoritarian impulses, because god alive, are they overwhelming.

Nicolai Kraus

unread,
Apr 26, 2022, 3:10:00 PM4/26/22
to Homotopy Type Theory
Mike has done a lot for our community and enjoys enormous respect; he doesn't need anonymous people on the internet to "stand up for him". While even the best of us make mistakes and people were hurt, Mike has apologised for that weeks ago. Out of respect for people who were hurt, I supported the decision of the HoTTEST organisers to not hold the distinguished lecture series in the immediate aftermath of the discussion, but I all the more look forward to finally being able to attend Mike's talks [1].

With regards to the recent statements by David, I want to remark that our community has always been civilised and polite. Thus, we did not have to learn a fundamental rule of online discussions: Don't feed the troll [1]. Nobody here needs to defend themselves against David's baseless accusations and insults.

Nicolai

[1] https://groups.google.com/g/HomotopyTypeTheory/c/m3hQAKtypJs/m/0FREJL8gAAAJ
[2] https://en.wiktionary.org/wiki/don%27t_feed_the_troll

Andrej Bauer

unread,
Apr 27, 2022, 7:00:59 AM4/27/22
to Homotopy Type Theory
This mailing list is a community service. The present discussion has run its course and is not contributing anything to the community anymore. At present its only purpose is bickering and reiterating of opinions that have already been stated multiple times. I am therefore locking it.

The mailing list owner,

Andrej Bauer

Reply all
Reply to author
Forward
This conversation is locked
You cannot reply and perform actions on locked conversations.
0 new messages