From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 8204 invoked from network); 5 May 2022 02:04:52 -0000 Received: from mail-io1-xd38.google.com (2607:f8b0:4864:20::d38) by inbox.vuxu.org with ESMTPUTF8; 5 May 2022 02:04:52 -0000 Received: by mail-io1-xd38.google.com with SMTP id y13-20020a056602164d00b0065a9dec1ef2sf2043779iow.23 for ; Wed, 04 May 2022 19:04:52 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1651716290; cv=pass; d=google.com; s=arc-20160816; b=t85vyPas9waXpNukewy8UVBwHTz76ysM0OFyBXmN4xGp9+G9mnijJ8Z6+PwS7cSaSM x537OLyqODuJgbKyBJpj4fJmIcUYCqS7jGTopjZUFOgMLVJIXR46wzR+Gvt7jrrFTI4z FDqgQAHkxdIDOgfQFPK+G7XBFXBu92rpCwDKYXjkDWHWy84xbHsK+iyvvVm6GXBuOHLH jM3YqFQWWNDeZosFBxV53Wi7wvwSDJyPFaSxHI4LMNysD2yQ79LRqOAqkvBn33bwUHMa Lozf9QeSCBmh/SKeZlVFpnf8BEh9WIKRjhepG9i9SNpPJBqe7oopzjkK/HAKdTpLLBiq 4xew== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:to:in-reply-to:references :message-id:date:subject:mime-version:from:content-transfer-encoding :sender:dkim-signature; bh=SDJ7pUQVwnFqXNmD/1eN7T5cSMFh4VE8F131xLMQ/4k=; b=tw/Jb2JZNVZbyQkibHzN4vJ49vhf0sJ8aIcvyRLvHGpxYXCOC3ZVp99W4CFNdusPLN N1Z+zyjVpnca8gjdPNcXCo3c6wrFYY4Mk0cU71f+mmFQSktWAiAfeDpV55d76KbUGcdI 4iPAy6eQo/6wv8HzqOBUkEVTvAsRWLHjQt2fFA6JV7PJQp3QMJdETsk39MzmmUd4YbXS aKKwwGdMAN+LrfdHtStJcbssE5jUZ5tWqeRSuyh42yL/4avSxTlNmNJyj7aPjBEcsYM7 6Ysj8JeRs07EwXEYDsmdnkUavuUzblWUtTJqp25dfP9y56gdDn8FL8d3cdCP2q0FQCR7 DL7A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=IyJzGPAb; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f30 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:content-transfer-encoding:from:mime-version:subject:date :message-id:references:in-reply-to:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=SDJ7pUQVwnFqXNmD/1eN7T5cSMFh4VE8F131xLMQ/4k=; b=JnvXaNV2Gd3sG33ZcOGDpBY0oY0J6iqwdSuvdn9ApsldbeQpDnbeNwhnMCjczROYsD e5WRI8MjTS7fLZmyhyA5z+DQ6ZcA/RVCU8sXrChZ6eiXH1x+Gqo3az3tBv0jLT22jOZJ ZKGrfr8JL5wr5vfL0fCwmXoE9y7DK2TxzDiaPgmXNVDk37yH/B/CUD2tYLxRJ5glFHxu 0OBaX1AQFdX2srCajxvA/gibSl6MsSctpfQXA7KJjVOQpKD9uud7zS/s10nuYHfKsodj FaiQG6VorjWYq/Z0wE+gkRL1O9gLfKXU8PgkmgkGI8ofVgbIQ/PODqNrsdixTDTNecQA jghg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:content-transfer-encoding:from :mime-version:subject:date:message-id:references:in-reply-to:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=SDJ7pUQVwnFqXNmD/1eN7T5cSMFh4VE8F131xLMQ/4k=; b=GkLyjnzlYyPgozW9agE+YoPf0Ah4h/abruocyBXZ0PVyRKRZSMB3hAPhb0DXZu8aAc LdPsaoZaGwZPkbhpNpbN/9KOu32DuudaUFTpIltOLixFrAckPONPeDZRO+XgSaI0LuOu Ty5wR+KeW2t9+vfHqwQiY5zIzq6QipqfyrJFYvXq6yNPo/x8S6Riy01LVA3ruHhUrB0Z Fzgg3xpj4TYNCyqIUARPwZJEHosh+QEOgscY6mW4eq4Rpq/itDaXK2nj410j05ard48u K2jQGswFuUW6RyZcWPI7TQ607SxEWOeMb8y3BEnPimG30JAXJ1sDYoqIzfwh51wIHmh9 jX1g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533Chfh6YxrvXHv758SoDhN5s+Gv21GO6zBlCNq7sxbTscF/EbHp WI4X4DFQ8LJlPi0eMhiTDGA= X-Google-Smtp-Source: ABdhPJwVHBznS5bt4gFUCAk+4LupqvcXvUFXAK4yE0ZIbt0U0/0JjY6lyYOV7BJ/TxOvpoC/3tcnxw== X-Received: by 2002:a05:6e02:12b4:b0:2ca:e755:ee4a with SMTP id f20-20020a056e0212b400b002cae755ee4amr10184393ilr.65.1651716289684; Wed, 04 May 2022 19:04:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a02:6f4d:0:b0:326:5851:8cdf with SMTP id b13-20020a026f4d000000b0032658518cdfls646406jae.11.gmail; Wed, 04 May 2022 19:04:48 -0700 (PDT) X-Received: by 2002:a02:6a60:0:b0:315:4758:1be1 with SMTP id m32-20020a026a60000000b0031547581be1mr10546853jaf.316.1651716288445; Wed, 04 May 2022 19:04:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1651716288; cv=none; d=google.com; s=arc-20160816; b=JfNkRlDPbwLoDmUZbyotDdERxn0YbFyMnLYpnbd9ay5rnQ8NgKvNdyt7WNil6gRZL0 9TXbCEnaNovowUvXXEU7LvM2iOLoT9ecQB+4iMV8Asi1WF1l9PjWmg4nnbimlzYUwyhC FjYiv1m0PmRi+xbLlzV5ByvfKwxOCu60TkPY6ENXxDZXrZ+gMe00taN2Yfqq5XEn87S+ V4czxRY8T9H0GNBOv6Sc4toHrhN0G8+btJiwmeI15aipIjoDyCe7fVsN4iRuXMjuBR1N hGJUxMVdibBf7XBJRQN79VTzrMG7KisQT1OcReUg50FbVW3m980ylKAVkkAiKlO+klTO aSyw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:references:message-id:date:subject:mime-version:from :content-transfer-encoding:dkim-signature; bh=pfqLW/d3ZO2PlCT8ZRjlFtGjkx8MQeJ5qOFKYL9FHrc=; b=g/boCFXjSVebDHjyTZkUUoKCPfcseJ3V2SZEiHGDwt0OOBGFqX9KGyLkXNjFu/irbo M2Pp14nGN03PXQxac+SHvg9RH2stMenzPKKIwvNl8pfKQLtfBKnIHyoSkd9P1W0hsV54 q5ObOYSuVJCFfBjuZFu6SPTBFu4v1iSPOSo2t35ZH5X5KO6F3OQK5Js7zubBKw5cjHA0 DX77FnuSQXKkm+/Eprot8QgvSkN1zBnOQCCOswb/ahX9gIQCjb57HQIWxm3rXh/PcLcy EUSIKbpoBzx7LcvFRtkjFB6aC/imV0aw9kQDKHNk8uWkvqiIWQIm/VNwJmKtKYOiSobd qZ2w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=IyJzGPAb; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f30 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-qv1-xf30.google.com (mail-qv1-xf30.google.com. [2607:f8b0:4864:20::f30]) by gmr-mx.google.com with ESMTPS id i21-20020a056638381500b0032b603bf16esi66047jav.2.2022.05.04.19.04.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 04 May 2022 19:04:48 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f30 as permitted sender) client-ip=2607:f8b0:4864:20::f30; Received: by mail-qv1-xf30.google.com with SMTP id kj8so2106680qvb.6 for ; Wed, 04 May 2022 19:04:48 -0700 (PDT) X-Received: by 2002:a05:6214:1cc4:b0:431:4cbc:1d91 with SMTP id g4-20020a0562141cc400b004314cbc1d91mr20152519qvd.64.1651716287554; Wed, 04 May 2022 19:04:47 -0700 (PDT) Received: from smtpclient.apple ([2600:381:710b:beeb:f4a5:9f28:7d20:df2f]) by smtp.gmail.com with ESMTPSA id f3-20020ac84643000000b002f39b99f671sm127095qto.11.2022.05.04.19.04.46 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 04 May 2022 19:04:47 -0700 (PDT) Content-Type: multipart/alternative; boundary=Apple-Mail-E768E63B-0DBB-4794-B3AE-357B7A719910 Content-Transfer-Encoding: 7bit From: Steve Awodey Mime-Version: 1.0 (1.0) Subject: [HoTT] CMU HoTT Seminar Online: M. Shulman, Towards Third-Generation HOTT, May 5 & 12 Date: Wed, 4 May 2022 22:04:46 -0400 Message-Id: <3414F36F-65AB-43B4-B09B-944D08934FE5@cmu.edu> References: <3AAA7A5E-5AE6-4654-87E2-2687F34F9ADE@cmu.edu> In-Reply-To: <3AAA7A5E-5AE6-4654-87E2-2687F34F9ADE@cmu.edu> To: categories net , Homotopy Type Theory , CMUHoTT X-Mailer: iPhone Mail (19D52) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=IyJzGPAb; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f30 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , --Apple-Mail-E768E63B-0DBB-4794-B3AE-357B7A719910 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 h= ave > 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 --=20 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 e= mail 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. --Apple-Mail-E768E63B-0DBB-4794-B3AE-357B7A719910 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Reminder: Part II, May 5. 

~~~~~~~~ 

CMU HoTT Seminar Online 

~~~~~~~~
Mike Shulman (University of San Diego).
Apr= il 28, May 5, May 12
11:30am-1:00pm EST (UTC-04:00)
Join Zoom Meeting=
https://cmu.zo= om.us/j/622894049
Meeting ID: 622 894 049
Passcode: Brunerie's nu= mber
Mike Shulman
University of San Diego
Towards Third-Generation= HOTT


On Apr 23, 20= 22, at 14:15, Steve Awodey <awodey@cmu.edu> wrote:

=EF=BB=BF~*~*~*~*~= *~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~
Mike Shulman (University of San Diego).
April 28, Ma= y 5, May 12
11:30am-1:00pm EST (UTC-04:00)
=
Join Zoom Meeting
https://cmu.zoom.us/j/62= 2894049

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 iden= tity uniformly, but using paths instead.
This makes more eq= ualities definitional, and enables a form of
univalence tha= t computes; but requires inserting all the higher
structure= by hand with Kan operations.

I will prese= nt work in progress towards a third kind of homotopy type
t= heory, which we call Higher Observational Type Theory (HOTT). In this
system, identity is not defined uniformly across all types, but<= /span>
recursively for each type former: identifications of pairs = are pairs
of identifications, identifications of functions = are pointwise
identifications, and so on. Univalence is the= n just the instance of
this principle for the universe. The= resulting theory has many useful
definitional equalities l= ike cubical type theories, but also gives
rise to higher st= ructure automatically like Book HoTT. Also like Book
HoTT, = it can be interpreted in a class of model categories that
s= uffice 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 Ambr= us Kaposi.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail 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.
--Apple-Mail-E768E63B-0DBB-4794-B3AE-357B7A719910--