From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10736 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, May 5 & 12 Date: Wed, 4 May 2022 22:04:46 -0400 Message-ID: Reply-To: Steve Awodey Mime-Version: 1.0 (1.0) Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: 7bit Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="6734"; mail-complaints-to="usenet@ciao.gmane.io" To: categories net Original-X-From: majordomo@rr.mta.ca Thu May 05 15:12: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 1nmbHP-0001ZX-Js for gsmc-categories@m.gmane-mx.org; Thu, 05 May 2022 15:12:27 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:59122) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1nmbFf-00012t-8K; Thu, 05 May 2022 10:10:39 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1nmbFK-0002Xf-Qu for categories-list@rr.mta.ca; Thu, 05 May 2022 10:10:18 -0300 Original-Content-Transfer-Encoding: quoted-printable Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10736 Archived-At: [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 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/ ]