CMU HoTT Seminar Online: M. Shulman, Towards Third-Generation HOTT, May 5 & 12

[Steve Awodey <awodey@cmu.edu>]

[Note from moderator: Since I will be mostly without suitable internet 
access for several days, list service may be unavailable until May 11.]

Reminder: Part II, May 5.=20
~~~~~~~~=20
CMU HoTT Seminar Online=20
~~~~~~~~
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

> On Apr 23, 2022, at 14:15, Steve Awodey <awodey@cmu.edu> wrote:
>=20
> =EF=BB=BF~*~*~*~*~*~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~
>=20
> Mike Shulman (University of San Diego).
> April 28, May 5, May 12
> 11:30am-1:00pm EST (UTC-04:00)
>=20
> Join Zoom Meeting
> https://cmu.zoom.us/j/622894049
>=20
> Meeting ID: 622 894 049
> Passcode: the Brunerie number
>=20
> ************************************************************
>=20
> Mike Shulman
> University of San Diego
>=20
> Towards Third-Generation HOTT
>=20
> 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.
>=20
> 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 (=E2=88=9E,1)-toposes; and we ha=
ve
> high hopes that, like cubical type theories, some version of it will
> satisfy canonicity and normalization.
>=20
> This is joint work with Thorsten Altenkirch and Ambrus Kaposi.
>=20

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]