* [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
@ 2022-04-11 13:32 Chris Kapulkin
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
2022-04-14 15:49 ` Joyal, André
0 siblings, 2 replies; 22+ messages in thread
From: Chris Kapulkin @ 2022-04-11 13:32 UTC (permalink / raw)
To: HoTT Electronic Seminar Talks, Homotopy Type Theory, categories
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3MVeK4auqO3MTkjn0JBO0XoqV8k-5RnS%3DOfi%3DVDQv15DA%40mail.gmail.com.
^ permalink raw reply [flat|nested] 22+ messages in thread
* [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-11 13:32 [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Chris Kapulkin
@ 2022-04-14 1:28 ` Chris Kapulkin
2022-04-14 8:32 ` 'Thorsten Altenkirch' via Homotopy Type Theory
` (4 more replies)
2022-04-14 15:49 ` Joyal, André
1 sibling, 5 replies; 22+ messages in thread
From: Chris Kapulkin @ 2022-04-14 1:28 UTC (permalink / raw)
To: HoTT Electronic Seminar Talks, Homotopy Type Theory, categories
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 <k.kapulkin@gmail.com> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3Pjt4%3Dwi5ikinGTqkKXyQKQ6iWOCtyTjz%3DBc1zufLz-AQ%40mail.gmail.com.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
@ 2022-04-14 8:32 ` 'Thorsten Altenkirch' via Homotopy Type Theory
2022-04-14 9:25 ` 'Urs Schreiber' via Homotopy Type Theory
` (3 subsequent siblings)
4 siblings, 0 replies; 22+ messages in thread
From: 'Thorsten Altenkirch' via Homotopy Type Theory @ 2022-04-14 8:32 UTC (permalink / raw)
To: Chris Kapulkin, HoTT Electronic Seminar Talks,
Homotopy Type Theory, categories
[-- Attachment #1: Type: text/plain, Size: 5406 bytes --]
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
From: homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> on behalf of Chris Kapulkin <k.kapulkin@gmail.com>
Date: Thursday, 14 April 2022 at 02:28
To: HoTT Electronic Seminar Talks <hott-electronic-seminar-talks@googlegroups.com>, Homotopy Type Theory <homotopytypetheory@googlegroups.com>, categories@mta.ca <categories@mta.ca>
Subject: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
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 <k.kapulkin@gmail.com> 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 HomotopyTypeTheory+unsubscribe@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.
--
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/PAXPR06MB78693E007AE2B907EE128D6ACDEF9%40PAXPR06MB7869.eurprd06.prod.outlook.com.
[-- Attachment #2: Type: text/html, Size: 9152 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
2022-04-14 8:32 ` 'Thorsten Altenkirch' via Homotopy Type Theory
@ 2022-04-14 9:25 ` 'Urs Schreiber' via Homotopy Type Theory
2022-04-14 10:42 ` Thomas Streicher
` (2 subsequent siblings)
4 siblings, 0 replies; 22+ messages in thread
From: 'Urs Schreiber' via Homotopy Type Theory @ 2022-04-14 9:25 UTC (permalink / raw)
To: Chris Kapulkin
Cc: HoTT Electronic Seminar Talks, Homotopy Type Theory, categories
On Thu, Apr 14, 2022 at 5:28 AM Chris Kapulkin <k.kapulkin@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.
--
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/CA%2BKbugem61xD06bxhHvd5vuUJdHrt%2BCJu0%2BYoJvNBM57jCxJCA%40mail.gmail.com.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
2022-04-14 8:32 ` 'Thorsten Altenkirch' via Homotopy Type Theory
2022-04-14 9:25 ` 'Urs Schreiber' via Homotopy Type Theory
@ 2022-04-14 10:42 ` Thomas Streicher
2022-04-14 11:48 ` Andrej Bauer
2022-04-14 20:23 ` Nicolas Alexander Schmidt
4 siblings, 0 replies; 22+ messages in thread
From: Thomas Streicher @ 2022-04-14 10:42 UTC (permalink / raw)
To: Chris Kapulkin
Cc: HoTT Electronic Seminar Talks, Homotopy Type Theory, categories
> 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
--
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/20220414104239.GA29083%40mathematik.tu-darmstadt.de.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
` (2 preceding siblings ...)
2022-04-14 10:42 ` Thomas Streicher
@ 2022-04-14 11:48 ` Andrej Bauer
2022-04-14 15:49 ` Martín Hötzel Escardó
2022-04-14 20:23 ` Nicolas Alexander Schmidt
4 siblings, 1 reply; 22+ messages in thread
From: Andrej Bauer @ 2022-04-14 11:48 UTC (permalink / raw)
To: HoTT Electronic Seminar Talks, Homotopy Type Theory, categories
[-- Attachment #1: Type: text/plain, Size: 2479 bytes --]
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
<https://github.com/HoTT/book/pull/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
<https://github.com/HoTT/book/issues/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
--
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/CAB0nkh2xM3m9A61Y5Pp5XbzH88SWSZy7gPqxkJxX%2BQTPLWXQ3w%40mail.gmail.com.
[-- Attachment #2: Type: text/html, Size: 3089 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-11 13:32 [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Chris Kapulkin
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
@ 2022-04-14 15:49 ` Joyal, André
1 sibling, 0 replies; 22+ messages in thread
From: Joyal, André @ 2022-04-14 15:49 UTC (permalink / raw)
To: Chris Kapulkin, HoTT Electronic Seminar Talks,
Homotopy Type Theory, categories
[-- Attachment #1: Type: text/plain, Size: 3953 bytes --]
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 : homotopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com> de la part de Chris Kapulkin <k.kapulkin@gmail.com>
Envoyé : 11 avril 2022 09:32
À : HoTT Electronic Seminar Talks <hott-electronic-seminar-talks@googlegroups.com>; Homotopy Type Theory <homotopytypetheory@googlegroups.com>; categories@mta.ca <categories@mta.ca>
Objet : [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAEXhy3MVeK4auqO3MTkjn0JBO0XoqV8k-5RnS%3DOfi%3DVDQv15DA%40mail.gmail.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/QB1PR01MB2948B2FA84E4733851CA50F4FDEF9%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM.
[-- Attachment #2: Type: text/html, Size: 7190 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-14 11:48 ` Andrej Bauer
@ 2022-04-14 15:49 ` Martín Hötzel Escardó
0 siblings, 0 replies; 22+ messages in thread
From: Martín Hötzel Escardó @ 2022-04-14 15:49 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 3295 bytes --]
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
1.
On Thursday, 14 April 2022 at 12:49:15 UTC+1 Andrej Bauer wrote:
> 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
> <https://github.com/HoTT/book/pull/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
> <https://github.com/HoTT/book/issues/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
>
>
>
>
>
--
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/cdf9c1ad-5c35-4751-9d3d-e2621b71fb12n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 4671 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
` (3 preceding siblings ...)
2022-04-14 11:48 ` Andrej Bauer
@ 2022-04-14 20:23 ` Nicolas Alexander Schmidt
2022-04-15 3:00 ` [HoTT] " Alexander Kurz
4 siblings, 1 reply; 22+ messages in thread
From: Nicolas Alexander Schmidt @ 2022-04-14 20:23 UTC (permalink / raw)
To: HomotopyTypeTheory
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 <k.kapulkin@gmail.com> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/876f6e58-211c-4824-e938-4b915e18d859%40fromzerotoinfinity.xyz.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-14 20:23 ` Nicolas Alexander Schmidt
@ 2022-04-15 3:00 ` Alexander Kurz
2022-04-15 9:29 ` Josh Chen
0 siblings, 1 reply; 22+ messages in thread
From: Alexander Kurz @ 2022-04-15 3:00 UTC (permalink / raw)
To: HomotopyTypeTheory
I would love to hear Mike's lectures.
All the best wishes,
Alexander
> On Apr 14, 2022, at 13:23, Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz> 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 <k.kapulkin@gmail.com> 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 HomotopyTypeTheory+unsubscribe@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/6A66F50E-FAF2-4C31-ABA9-835ED4FDE345%40gmail.com.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-15 3:00 ` [HoTT] " Alexander Kurz
@ 2022-04-15 9:29 ` Josh Chen
2022-04-15 11:21 ` Ondrej Rypacek
2022-04-15 12:01 ` Martín Hötzel Escardó
0 siblings, 2 replies; 22+ messages in thread
From: Josh Chen @ 2022-04-15 9:29 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 6501 bytes --]
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 <
> ze...@fromzerotoinfinity.xyz> 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 <k.kap...@gmail.com>
> 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.
[-- Attachment #1.2: Type: text/html, Size: 9056 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-15 9:29 ` Josh Chen
@ 2022-04-15 11:21 ` Ondrej Rypacek
2022-04-15 12:01 ` Martín Hötzel Escardó
1 sibling, 0 replies; 22+ messages in thread
From: Ondrej Rypacek @ 2022-04-15 11:21 UTC (permalink / raw)
To: Josh Chen; +Cc: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 7643 bytes --]
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 <jaycech3n@gmail.com> 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 <ze...@fromzerotoinfinity.xyz> 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 <k.kap...@gmail.com> 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.
[-- Attachment #2: Type: text/html, Size: 10773 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-15 9:29 ` Josh Chen
2022-04-15 11:21 ` Ondrej Rypacek
@ 2022-04-15 12:01 ` Martín Hötzel Escardó
2022-04-23 13:03 ` David
1 sibling, 1 reply; 22+ messages in thread
From: Martín Hötzel Escardó @ 2022-04-15 12:01 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1823 bytes --]
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
On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>
>
>
--
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/b5594a51-8412-412f-a3a2-da65b288a775n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 2406 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-15 12:01 ` Martín Hötzel Escardó
@ 2022-04-23 13:03 ` David
2022-04-23 19:36 ` Andreas Nuyts
0 siblings, 1 reply; 22+ messages in thread
From: David @ 2022-04-23 13:03 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 2810 bytes --]
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
On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com wrote:
> 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
>
> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>>
>>
>>
--
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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 3728 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-23 13:03 ` David
@ 2022-04-23 19:36 ` Andreas Nuyts
2022-04-25 9:36 ` David
0 siblings, 1 reply; 22+ messages in thread
From: Andreas Nuyts @ 2022-04-23 19:36 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 5876 bytes --]
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
On 23.04.22 15:03, David wrote:
> 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
>
> On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com wrote:
>
> 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
>
> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>
>
> --
> 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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/065d081e-b470-7f00-8090-a8cd15ed4592%40gmail.com.
[-- Attachment #2: Type: text/html, Size: 8356 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-23 19:36 ` Andreas Nuyts
@ 2022-04-25 9:36 ` David
2022-04-25 16:23 ` Josh Chen
0 siblings, 1 reply; 22+ messages in thread
From: David @ 2022-04-25 9:36 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 6801 bytes --]
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
On Saturday, April 23, 2022 at 8:36:55 PM UTC+1 anuyts wrote:
> 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
>
>
> On 23.04.22 15:03, David wrote:
>
> 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
>
> On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com wrote:
>
>> 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
>>
>> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>>>
>>>
>>> --
> 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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
>
>
--
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/8d56b68f-2473-4f50-9d00-28cc58fbd8e7n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 9823 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-25 9:36 ` David
@ 2022-04-25 16:23 ` Josh Chen
2022-04-25 19:25 ` David
0 siblings, 1 reply; 22+ messages in thread
From: Josh Chen @ 2022-04-25 16:23 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 8366 bytes --]
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.
On Monday, April 25, 2022 at 10:36:13 AM UTC+1 David wrote:
> 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
>
> On Saturday, April 23, 2022 at 8:36:55 PM UTC+1 anuyts wrote:
>
>> 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
>>
>>
>> On 23.04.22 15:03, David wrote:
>>
>> 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
>>
>> On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com wrote:
>>
>>> 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
>>>
>>> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>>>>
>>>>
>>>> --
>> 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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com
>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>>
>>
--
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/5595508f-15bd-42a2-a350-103647bfac1an%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 11499 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-25 16:23 ` Josh Chen
@ 2022-04-25 19:25 ` David
2022-04-26 1:18 ` Josh Chen
0 siblings, 1 reply; 22+ messages in thread
From: David @ 2022-04-25 19:25 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 9597 bytes --]
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
On Monday, April 25, 2022 at 5:23:56 PM UTC+1 Josh Chen wrote:
> 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.
> On Monday, April 25, 2022 at 10:36:13 AM UTC+1 David wrote:
>
>> 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
>>
>> On Saturday, April 23, 2022 at 8:36:55 PM UTC+1 anuyts wrote:
>>
>>> 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
>>>
>>>
>>> On 23.04.22 15:03, David wrote:
>>>
>>> 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
>>>
>>> On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com
>>> wrote:
>>>
>>>> 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
>>>>
>>>> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>>>>>
>>>>>
>>>>> --
>>> 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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com
>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>>>
>>>
--
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/d3e7bfdf-9953-4e9b-8720-7fcd9ef9ae22n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 14028 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-25 19:25 ` David
@ 2022-04-26 1:18 ` Josh Chen
2022-04-26 2:04 ` David
0 siblings, 1 reply; 22+ messages in thread
From: Josh Chen @ 2022-04-26 1:18 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 11212 bytes --]
> 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".
On Monday, April 25, 2022 at 8:25:21 PM UTC+1 David wrote:
> 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
>
>
>
> On Monday, April 25, 2022 at 5:23:56 PM UTC+1 Josh Chen wrote:
>
>> 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.
>> On Monday, April 25, 2022 at 10:36:13 AM UTC+1 David wrote:
>>
>>> 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
>>>
>>> On Saturday, April 23, 2022 at 8:36:55 PM UTC+1 anuyts wrote:
>>>
>>>> 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
>>>>
>>>>
>>>> On 23.04.22 15:03, David wrote:
>>>>
>>>> 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
>>>>
>>>> On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com
>>>> wrote:
>>>>
>>>>> 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
>>>>>
>>>>> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>>>>>>
>>>>>>
>>>>>> --
>>>> 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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com
>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>> .
>>>>
>>>>
>>>>
--
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/f3b09b31-d4b3-4a4f-8728-dec347c2e574n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 15741 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-26 1:18 ` Josh Chen
@ 2022-04-26 2:04 ` David
2022-04-26 19:10 ` Nicolai Kraus
0 siblings, 1 reply; 22+ messages in thread
From: David @ 2022-04-26 2:04 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 13374 bytes --]
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.
On Tuesday, April 26, 2022 at 2:18:59 AM UTC+1 Josh Chen wrote:
> > 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".
> On Monday, April 25, 2022 at 8:25:21 PM UTC+1 David wrote:
>
>> 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
>>
>>
>>
>> On Monday, April 25, 2022 at 5:23:56 PM UTC+1 Josh Chen wrote:
>>
>>> 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.
>>> On Monday, April 25, 2022 at 10:36:13 AM UTC+1 David wrote:
>>>
>>>> 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
>>>>
>>>> On Saturday, April 23, 2022 at 8:36:55 PM UTC+1 anuyts wrote:
>>>>
>>>>> 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
>>>>>
>>>>>
>>>>> On 23.04.22 15:03, David wrote:
>>>>>
>>>>> 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
>>>>>
>>>>> On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com
>>>>> wrote:
>>>>>
>>>>>> 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
>>>>>>
>>>>>> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>>>>>>>
>>>>>>>
>>>>>>> --
>>>>> 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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com
>>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>>> .
>>>>>
>>>>>
>>>>>
--
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/e471240c-6a31-4325-834b-c38230252e60n%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 18083 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-26 2:04 ` David
@ 2022-04-26 19:10 ` Nicolai Kraus
2022-04-27 11:00 ` Andrej Bauer
0 siblings, 1 reply; 22+ messages in thread
From: Nicolai Kraus @ 2022-04-26 19:10 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 14694 bytes --]
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
On Tuesday, April 26, 2022 at 3:04:20 AM UTC+1 David wrote:
> 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.
> On Tuesday, April 26, 2022 at 2:18:59 AM UTC+1 Josh Chen wrote:
>
>> > 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".
>> On Monday, April 25, 2022 at 8:25:21 PM UTC+1 David wrote:
>>
>>> 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
>>>
>>>
>>>
>>> On Monday, April 25, 2022 at 5:23:56 PM UTC+1 Josh Chen wrote:
>>>
>>>> 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.
>>>> On Monday, April 25, 2022 at 10:36:13 AM UTC+1 David wrote:
>>>>
>>>>> 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
>>>>>
>>>>> On Saturday, April 23, 2022 at 8:36:55 PM UTC+1 anuyts wrote:
>>>>>
>>>>>> 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
>>>>>>
>>>>>>
>>>>>> On 23.04.22 15:03, David wrote:
>>>>>>
>>>>>> 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
>>>>>>
>>>>>> On Friday, April 15, 2022 at 1:01:12 PM UTC+1 escardo...@gmail.com
>>>>>> wrote:
>>>>>>
>>>>>>> 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
>>>>>>>
>>>>>>> On Friday, 15 April 2022 at 10:29:41 UTC+1 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
>>>>>>>>
>>>>>>>>
>>>>>>>> --
>>>>>> 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/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com
>>>>>> <https://groups.google.com/d/msgid/HomotopyTypeTheory/bfd91d1f-da88-4cbb-97ed-df868f6e7190n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>>>> .
>>>>>>
>>>>>>
>>>>>>
--
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/f0c76011-11c2-4642-a67d-502ce8fb485cn%40googlegroups.com.
[-- Attachment #1.2: Type: text/html, Size: 19228 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
2022-04-26 19:10 ` Nicolai Kraus
@ 2022-04-27 11:00 ` Andrej Bauer
0 siblings, 0 replies; 22+ messages in thread
From: Andrej Bauer @ 2022-04-27 11:00 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 729 bytes --]
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
--
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/CAB0nkh088mBUrQ3eQyLPFD1xRkoHgF9G9oHiMgELTaxw3h18bA%40mail.gmail.com.
[-- Attachment #2: Type: text/html, Size: 1104 bytes --]
^ permalink raw reply [flat|nested] 22+ messages in thread
end of thread, other threads:[~2022-04-27 11:00 UTC | newest]
Thread overview: 22+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-04-11 13:32 [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Chris Kapulkin
2022-04-14 1:28 ` [HoTT] " Chris Kapulkin
2022-04-14 8:32 ` 'Thorsten Altenkirch' via Homotopy Type Theory
2022-04-14 9:25 ` 'Urs Schreiber' via Homotopy Type Theory
2022-04-14 10:42 ` Thomas Streicher
2022-04-14 11:48 ` Andrej Bauer
2022-04-14 15:49 ` Martín Hötzel Escardó
2022-04-14 20:23 ` Nicolas Alexander Schmidt
2022-04-15 3:00 ` [HoTT] " Alexander Kurz
2022-04-15 9:29 ` Josh Chen
2022-04-15 11:21 ` Ondrej Rypacek
2022-04-15 12:01 ` Martín Hötzel Escardó
2022-04-23 13:03 ` David
2022-04-23 19:36 ` Andreas Nuyts
2022-04-25 9:36 ` David
2022-04-25 16:23 ` Josh Chen
2022-04-25 19:25 ` David
2022-04-26 1:18 ` Josh Chen
2022-04-26 2:04 ` David
2022-04-26 19:10 ` Nicolai Kraus
2022-04-27 11:00 ` Andrej Bauer
2022-04-14 15:49 ` Joyal, André
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).