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

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

[Steve Awodey]

[-- Attachment #1: Type: text/plain, Size: 2763 bytes --]

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

> On Apr 23, 2022, at 14:15, Steve Awodey <awodey@cmu.edu> wrote:
> 
> ~*~*~*~*~*~*~*~* 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: the Brunerie 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.
> 
> 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/3414F36F-65AB-43B4-B09B-944D08934FE5%40cmu.edu.

[-- Attachment #2: Type: text/html, Size: 4874 bytes --]