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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 7382 invoked from network); 22 Apr 2022 20:51:21 -0000 Received: from mail-pf1-x43a.google.com (2607:f8b0:4864:20::43a) by inbox.vuxu.org with ESMTPUTF8; 22 Apr 2022 20:51:21 -0000 Received: by mail-pf1-x43a.google.com with SMTP id i18-20020a056a00225200b0050abac0449bsf6065455pfu.20 for ; Fri, 22 Apr 2022 13:51:21 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1650660680; cv=pass; d=google.com; s=arc-20160816; b=swoKjY1Z/iuSf7s5c7ehfZ21FR88BFMlpHoUnnzfMVecXg4/cFahsXgN4QbmkcQfgw 6SjOUAJcHMp9B1FcWAf+1BacEq/yQQF5qG7yfGD7uNBo6kJSL141xhPP1utJfjIo+g/w omHUfLeNIUMefSzHm3bSfkKJcWTPlWg46bXuJ9LLw+kKKvUyY9tt+batD9aiP5OS0foq 2pQ83cyg5MQQhtS5k8MteNoHNDuHtxmlulUv5JOfGNU7ctg9u91rhu7D3CJY6Tf2SiHc rn/Slz1YenuaNMa6LTg8bwGyd/qGzUvJvu9C7tds2sxqeSvB22gEp48XOCDexDKeXd+5 HMAQ== 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:cc:date:message-id:subject :mime-version:content-transfer-encoding:from:sender:dkim-signature; bh=p3fzQsTXbq4aFW9OrR7KDZz94E+yFm8eOG1dq1mo9Dk=; b=jG5/GuU1ttHhkwApqpDplgzlpHSjokG5ulmhHG8GHHe4TFHZvx3wHMMRmmSUBL70kX BeiuvDlkFkNT3GCYnENuQlCitoJkkhxQQDYB77BmhZ7+hhhK0plUKMop486ui9y5ZxZQ QU6lLB68HD3ofq+72gRBOl+50a3WfeGHv+dlIb10+UUlpbnSyk0ZY17Z+TENv6WvA6fQ FJ49D+lRUedtPceflXRBYGfzPyPtrcGXlo/SLZlcqLmL4gZakifY95jX+WM1s1ct8Brw puMJXigkYaYZRh6+4sr8rtBA45KeEEi0RiBecR2a72mIQiSPH9juYCGnnH6RxEWx3xZw u88g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=OzMqpJfC; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::731 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:from:content-transfer-encoding:mime-version:subject :message-id:date:cc:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=p3fzQsTXbq4aFW9OrR7KDZz94E+yFm8eOG1dq1mo9Dk=; b=cjmzkLgLnKTOvxsa46j99MGq/d0M1A+aaRhfYkuU/rH/8n7QwK9GOb+qoG3oukwNb2 OR0IbN4Uvcd67twb9NpMge2f/ahhskKDu3i6UB+dtTmgElV0al8DOTksmJ9TeOmQhclq G6+XSYaPN6I0PvjzxE1WctvYzB9efHmvxQXcwAmNhVRu1R7d4B1FwX7iKLuAnCbEucgZ GomheNgrPokAKBpxgrGbXBZ5sjajIqdjq9qutU4KqC+29DrRfmyQ4+XwJ/p/I3q4Uzdg vR2LilW8KmtH+5Rszmxksf2lHZtp2QgEAJVFp6qJvf1d9KWslCwsKe9/BuBqdpE4SoA+ 5NOg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:from:content-transfer-encoding :mime-version:subject:message-id:date:cc: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=p3fzQsTXbq4aFW9OrR7KDZz94E+yFm8eOG1dq1mo9Dk=; b=wgqROmi6Em1/543gD9HwSSKB2AuVLjU3A0VrUjT74tXC2LB36J9xRG9rHwpRAGrxzs 4auin9Tyr2Dh3KfI/9CsbU2QrInewMcPBmhbd2LAVe69s8u03Kc45AqwNJlryLo6oTDo gXywoI+FOGHQmhTLT/HCsJIrshFZb3PCfag5XWTSv7jlP+rRFyfYhmD31K0+bci5MoNt siND8cejssqu2HUBTHXd+IqMGRCA8/pr/gNpyEdJgBnILLGl6bM1BiaPazA0qtXrXrmT gmuliRdQEpnGQape8MBENvux6zWqquEtHsGKk5ikmUjpOvdmrvrYEPnNBSq0vBp+8krM yw4w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532xiUC+W1LQADe7hin7+aLrlzEDsz5ykDOptdsV3z8ly6vE7k9J RHImZQE1YjXvY3WgSdUaP0Y= X-Google-Smtp-Source: ABdhPJxDJ5HDyuJaxMVdtUZNLrD2XFj3JuC+GSuS2XFwkNtF0YWHBawGBR9ifQlDVvb/0KK30YULdQ== X-Received: by 2002:a63:4d66:0:b0:399:14fa:2acc with SMTP id n38-20020a634d66000000b0039914fa2accmr5491817pgl.558.1650660680544; Fri, 22 Apr 2022 13:51:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:903:186:b0:15a:2961:493b with SMTP id z6-20020a170903018600b0015a2961493bls8774732plg.10.gmail; Fri, 22 Apr 2022 13:51:19 -0700 (PDT) X-Received: by 2002:a17:90a:dd46:b0:1b8:8:7303 with SMTP id u6-20020a17090add4600b001b800087303mr18215766pjv.197.1650660678929; Fri, 22 Apr 2022 13:51:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1650660678; cv=none; d=google.com; s=arc-20160816; b=oUKLaqsgIJp8T9HEJw2BDW6wFH/UkQLA/6n8Q8XdJrlR5jHQ9wd1zINGBFOC/wNj+q fg5XHgq7a5NC9R75w3JUE+OAZNoWe0coitAZLrQ4YF8E9Xws+HM2SAmBf13qHwa/OLUZ zlwJ+mILE02XKtSwPyIqNDs+pNHvMCd2QACq/Xv9Ng2gfgr20pxz4RfnHNgS5ilqxzHt P4Lk56j2H1cOUNm2GGdW7RpI2iDthNl/vU84dLpWILwdhJDaSMEqcNt0YJ54w8AIguTr r6sh/M+JHwqpzP7fZsA7PuyuWOaGPxgp6ICSp4BF7rCaADJjsrhYAlEJP2rgPIZMTJzs T7eg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:cc:date:message-id:subject:mime-version :content-transfer-encoding:from:dkim-signature; bh=VTZbADGqX1xPtGhfwCg3y07kWmJFBm4nKTJrD0Bmhi8=; b=QOTt9lMU7heysivny1LPxH5Vfoa6p5Yre9MgPEUyizrGJ7TOOJkFRgvMxIUk+3+I0B GxaRgpXOnTPTy57okCZfLWQYcDbh19VoetNDgqppjrQARIEbiALtyj8yyc4zHaod+1gq 9JAg2+8aRQzFGB7fyoHjCyP6vC3VmDxTYmkKqKA9aZSTPKZl170m3rC+g2BKhrSFXRLF uq8z6ixU/8quE6F43tUwhg5IuVlljD8d7VCKdO+QTmpzQK6tcllu2ViS0PZAEvgVx673 p5oB8WfAYEtu4QqVpupyF8e7z5qXLBKQTg6xBi7boI16BY917efDsw3AhP+RnQ4AEVdQ rhww== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=OzMqpJfC; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::731 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-qk1-x731.google.com (mail-qk1-x731.google.com. [2607:f8b0:4864:20::731]) by gmr-mx.google.com with ESMTPS id o1-20020a62cd01000000b004fdca03b476si705194pfg.6.2022.04.22.13.51.18 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 22 Apr 2022 13:51:18 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::731 as permitted sender) client-ip=2607:f8b0:4864:20::731; Received: by mail-qk1-x731.google.com with SMTP id s70so6667396qke.8 for ; Fri, 22 Apr 2022 13:51:18 -0700 (PDT) X-Received: by 2002:a37:f71e:0:b0:69e:6240:aa with SMTP id q30-20020a37f71e000000b0069e624000aamr3787987qkj.679.1650660678134; Fri, 22 Apr 2022 13:51:18 -0700 (PDT) Received: from samson.phil.cmu.edu (SAMSON.PHIL.CMU.EDU. [128.2.65.128]) by smtp.gmail.com with ESMTPSA id b9-20020a05620a0f8900b0069e84c5352asm1336287qkn.47.2022.04.22.13.51.17 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 22 Apr 2022 13:51:17 -0700 (PDT) From: Steve Awodey Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.21\)) Subject: [HoTT] CORRECTION: CMU HoTT Seminar Online: M. Shulman, Towards Third-Generation HOTT, April 28, May 5 & 12 Message-Id: <24ABA61B-3514-413D-B6C4-01088430E779@cmu.edu> Date: Fri, 22 Apr 2022 16:51:16 -0400 Cc: EMILY RIEHL , Michael Shulman , =?utf-8?Q?Egbert=F0=9F=98=81_Rijke?= , Steve Awodey To: Homotopy Type Theory , CMU HoTT X-Mailer: Apple Mail (2.3445.104.21) 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=OzMqpJfC; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::731 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: , ~*~*~*~*~*~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~ Mike Shulman (University of San Diego). April 28, May 5 & 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 hav= e 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. --=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/24ABA61B-3514-413D-B6C4-01088430E779%40cmu.edu.