Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: "'Thorsten Altenkirch' via Homotopy Type Theory" <HomotopyTypeTheory@googlegroups.com>
To: Chris Kapulkin <k.kapulkin@gmail.com>,
	HoTT Electronic Seminar Talks
	<hott-electronic-seminar-talks@googlegroups.com>,
	Homotopy Type Theory <homotopytypetheory@googlegroups.com>,
	"categories@mta.ca" <categories@mta.ca>
Subject: Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series
Date: Thu, 14 Apr 2022 08:32:52 +0000	[thread overview]
Message-ID: <PAXPR06MB78693E007AE2B907EE128D6ACDEF9@PAXPR06MB7869.eurprd06.prod.outlook.com> (raw)
In-Reply-To: <CAEXhy3Pjt4=wi5ikinGTqkKXyQKQ6iWOCtyTjz=Bc1zufLz-AQ@mail.gmail.com>

[-- 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 --]

  reply	other threads:[~2022-04-14  8:33 UTC|newest]

Thread overview: 22+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-04-11 13:32 [HoTT] " Chris Kapulkin
2022-04-14  1:28 ` [HoTT] " Chris Kapulkin
2022-04-14  8:32   ` 'Thorsten Altenkirch' via Homotopy Type Theory [this message]
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é

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=PAXPR06MB78693E007AE2B907EE128D6ACDEF9@PAXPR06MB7869.eurprd06.prod.outlook.com \
    --to=homotopytypetheory@googlegroups.com \
    --cc=Thorsten.Altenkirch@nottingham.ac.uk \
    --cc=categories@mta.ca \
    --cc=hott-electronic-seminar-talks@googlegroups.com \
    --cc=k.kapulkin@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).