From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10724 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Steve Awodey Newsgroups: gmane.science.mathematics.categories Subject: CMU HoTT Seminar Online: M. Shulman, Towards Third-Generation HOTT, April 28, May 5 & 12 Date: Sat, 23 Apr 2022 14:15:01 -0400 Message-ID: Reply-To: Steve Awodey Mime-Version: 1.0 (1.0) Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="19034"; mail-complaints-to="usenet@ciao.gmane.io" To: categories net Original-X-From: majordomo@rr.mta.ca Sun Apr 24 01:15:28 2022 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1niOyN-0004j6-VQ for gsmc-categories@m.gmane-mx.org; Sun, 24 Apr 2022 01:15:28 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:58288) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1niOwj-0006pI-42; Sat, 23 Apr 2022 20:13:45 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1niOwQ-0002s7-FC for categories-list@rr.mta.ca; Sat, 23 Apr 2022 20:13:26 -0300 Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10724 Archived-At: =EF=BB=BF~*~*~*~*~*~*~*~* 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 (=E2=88=9E,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. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]