You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Steve Awodey (Apr 28 2022 at 12:42):~~~~~~~~ CMU HoTT Seminar Online ~~~~~~~~
Mike Shulman (University of San Diego).
April 28, May 5, May 12
11:30am-1:00pm EST (UTC-04:00)
Join Zoom Meeting
https://cmu.zoom.us/j/622894049
Meeting ID: 622 894 049
Passcode: Brunerie's number
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.
Ivan Di Liberti (Apr 28 2022 at 19:56):I could not join because of the time-zone. Is it going to appear on youtube? (Or somewhere)
Reid Barton (Apr 28 2022 at 22:07):https://www.youtube.com/watch?v=FrxkVzItMzA
Steve Awodey (May 05 2022 at 01:57):Reminder: Part II, May 5.
~~~~~~~~ CMU HoTT Seminar Online ~~~~~~~~
Mike Shulman (University of San Diego).
April 28, May 5, May 12
11:30am-1:00pm EST (UTC-04:00)
Join Zoom Meeting
https://cmu.zoom.us/j/622894049
Meeting ID: 622 894 049
Passcode: Brunerie's number
Mike Shulman
University of San Diego
Towards Third-Generation HOTT
Steve Awodey (May 09 2022 at 11:46):The recording from Mike Shulman's 2nd CMU HoTT Seminar is here:
https://www.youtube.com/watch?v=5ciDNfmvMdU
Steve Awodey (May 11 2022 at 11:31):Reminder: Part III, May 12.
~~~~~~~~ CMU HoTT Seminar Online ~~~~~~~~
Mike Shulman (University of San Diego)
Towards Third-Generation HOTT
April 28, May 5, May 12
11:30am-1:00pm EDT (UTC-04:00)
Join Zoom Meeting
https://cmu.zoom.us/j/622894049
Meeting ID: 622 894 049
Passcode: Brunerie's number