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

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