Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [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).