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 6659 invoked from network); 22 Apr 2022 20:44:39 -0000 Received: from mail-pf1-x43e.google.com (2607:f8b0:4864:20::43e) by inbox.vuxu.org with ESMTPUTF8; 22 Apr 2022 20:44:39 -0000 Received: by mail-pf1-x43e.google.com with SMTP id h66-20020a628345000000b0050ac8fa710esf6095666pfe.0 for ; Fri, 22 Apr 2022 13:44:39 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1650660278; cv=pass; d=google.com; s=arc-20160816; b=Ct9gUkRsj/CXwUQo30EsrvjCKLcWrGRVy3AB2ifF7DJU3WUI9OiicU94U+YNKJj1fp 4zBmUyNVh8GI4SjPx2blB2WO3EmVN4C9NrxYQK3dqssMGNsivC3AgqTJQmfusssVVeyj oWqBfAnmZy4TM+gsDT3Vp1/YiN11mi4NCh9zjPniFEYCbwf2oY3eYGAfp0BvhzOCW5FP TBf+fA4PoAwQ6ZA7lGKP0WqRarlGYNJpL3S+tYt6fY62BVxb+PzhtLQ4PLIHKG+QDSze SfqI8/FZ/tWWIzgknjy2Mk1ewbjj7j0ZftKc4eQ4IZ6TkGXDoj4CtoI1iZO1gQ2ilbZm tHDA== 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=YjqQO+lF8u+HVS8no59LEwCbW5Fl9ehP0yWTFKRLfNs=; b=q5E9WyTnuWpWHJe8crz5y3HozJXS7Um9DTyfBMaW8uRiBo1etITXzMUeIBb2rNvU16 p7MfJjE4ekDTE9bE9DoVa9A1BKpTIT/lBBJWZnmNOOedA+bZOgU6CQV8Um9gu1k8mbrQ Ge0lNdpehopcIs+AVPnEF5ucgp7f+l3vjCBRSWqpWqkO6lVVX0TXOLx9gZcJudHfeIsI kKEMD4vYn4q4TASaFzuuDTjfcXE/R8t0Nfr7UvZxwtG2s8hCBG/TSaL9AxvjRi9rFaXC 1BHi772x/2g7/WOthcly8m47eoNZCsfFkAwFZOfYvriI/2Y81fiAURsd33IGXyteydej 9/8A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=J+cjHQ3x; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f29 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=YjqQO+lF8u+HVS8no59LEwCbW5Fl9ehP0yWTFKRLfNs=; b=XqwKgXHahcMVBXRiGuR7AoxmfbMNOBArSFN79PKKJjGvJ1m9Mx+7vspvdKqYiSmME7 N0j9k5iAu062NMNtE2z2Jw1WUus2qJEevgtETRxTpWLvKR3ltoA5/5YBmeMe8nxJf9v2 w3kWZL0+2KjVrmwpHlj1IId+a5imm/9aXE3iZxzGxid7PVlWUTCM2P0lkyKiGuBF3SQ0 FHvwcH7pubzFLc4rJItddj9WXBMPhrbVWA7+T4en3dvDvHwLbGZm5+M8agl4fBAr69Zo mBlf4kkxAw3aiEKLI7ErDrmlOU55tvN6PVt9KMA0KbN25prplbTPEZQgTerV3iRw6P5+ dYvQ== 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=YjqQO+lF8u+HVS8no59LEwCbW5Fl9ehP0yWTFKRLfNs=; b=tTPLk/Vp1tzYkv4lNaq4YYMzJmYoQOswSij44pMZQsh8uvDMzzlECilBjYXGNlqoy4 2eDQ8npriLLd3/lyhkBCO4Rtw2h/rn9WNVIGtMg2DmUkDCdwXiU3qe6LRHvn7ZhdZFdC iLkXqAPChSFymeZ2CLKV3ag4qj3oH4w6YsVhu0o1Ga72i53+KaUO18X+jOryDqOJGNLr CPXPnwLUr2gKVmSHMkKYQC2MAlok16lixGoxk0VItYTW+Dneiiv6OF3Ppyi10ZSrqhaJ MbpTW0xsrHiaFqwMN5nzsRhbgEOncxJHeOjKKK1BwBY4CQifpqoNgU8q2ZwJZBPFuhTz GR4w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533oAEzzdiGZswEFaiHLQ/v52mVoykafvVtMq16wV3zeQ5KBiU2X 7R5Qnk0lyosNPeXQdk6iygg= X-Google-Smtp-Source: ABdhPJzOFgX+BK8O+AsKGFeOTswt5WD1srGeBYO8FGoaLG6XiCIaNafCLS/iO3pZnCTu3MLKNtv6nQ== X-Received: by 2002:a63:1325:0:b0:39d:8eaa:27f7 with SMTP id i37-20020a631325000000b0039d8eaa27f7mr5450758pgl.297.1650660277253; Fri, 22 Apr 2022 13:44:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:903:2447:b0:15c:3f58:ceec with SMTP id l7-20020a170903244700b0015c3f58ceecls2492644pls.3.gmail; Fri, 22 Apr 2022 13:44:35 -0700 (PDT) X-Received: by 2002:a17:90b:4b4f:b0:1d4:b9a9:84b8 with SMTP id mi15-20020a17090b4b4f00b001d4b9a984b8mr7348249pjb.138.1650660275540; Fri, 22 Apr 2022 13:44:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1650660275; cv=none; d=google.com; s=arc-20160816; b=mZiQxiRaTYn0FRoSglXYAkWFLJi1pMazuE7Mx4Pda+qgZ+q+l4UfyoYhnT5X+m2E72 ArQk7MrtZdM9RzirQUlWShUqh8M/UEfyjEtzkvYikMeC1qejJdoHMZ97v+b2rh8SpJ8B uAPwWn82zbzRO0q15QMG+s1XU1SvdVfRUEjzVMts7V+n+YaIvk6hrOaPZhvNdjaFcRWr nZuDkAds/UCEnCm425CSuZGw1rfLCLWibVNBgbqyXWhqNFpyCffTc7Wthm5bssesETta +y9BDqZiFvn8GuJ1JItTv8NJVQfXEZfemsZR195ZEKT8C8P2LeOtdks4kHribAz7BY7n LACw== 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=3SLZA50XWdMGCJKW7oqYvnszGhE2ihD08Uj1NIlirFM=; b=tnJ8pYm/UMa+pIgOBQgCVp4tbt6pKhKMgJDCpF+JKH+V/92tXSqY7jjDdYEwi0Kasx FhmszAqHUGp0zOm+2xwDYUJS+C3vH+RS8B54gFabkd4EAvS0WdIb1dimFE2mhlaR7r5p YXNFKo0EDpXpALtmY7XO1CMuiNS+C8wj+cZNFstXUNxXgnVAZWftcV/gro444BcaUvkM mLrxawksXMbBr9gBawbmdPaHOwoXNqhEibaz9HyqNA1I1by5SlyLFxoL1/EX5yJ8MuHj /jVbHiAI3jBig4EX3tC70SzUW/AkzdLwHgLzP/mt1fiFl5BnhOAy+TTyRFdHMVDL2Opa rQhQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=J+cjHQ3x; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f29 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-xf29.google.com (mail-qv1-xf29.google.com. [2607:f8b0:4864:20::f29]) by gmr-mx.google.com with ESMTPS id n2-20020a17090a9f0200b001cba62cfe78si1141412pjp.3.2022.04.22.13.44.35 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 22 Apr 2022 13:44:35 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f29 as permitted sender) client-ip=2607:f8b0:4864:20::f29; Received: by mail-qv1-xf29.google.com with SMTP id kd22so2054667qvb.4 for ; Fri, 22 Apr 2022 13:44:35 -0700 (PDT) X-Received: by 2002:a0c:b2d7:0:b0:443:afac:fc60 with SMTP id d23-20020a0cb2d7000000b00443afacfc60mr5177834qvf.58.1650660274335; Fri, 22 Apr 2022 13:44:34 -0700 (PDT) Received: from samson.phil.cmu.edu (SAMSON.PHIL.CMU.EDU. [128.2.65.128]) by smtp.gmail.com with ESMTPSA id m16-20020a05622a055000b002f35423f7c0sm1830544qtx.93.2022.04.22.13.44.33 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 22 Apr 2022 13:44:33 -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] CMU HoTT Seminar Online: M. Shulman, Towards Third-Generation HOTT, April 28, May 5 & 12 Message-Id: <141BA9BA-1B6F-4CD3-AB76-FAB0875A2C61@cmu.edu> Date: Fri, 22 Apr 2022 16:44:32 -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=J+cjHQ3x; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::f29 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 21, 28 and May 5 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/141BA9BA-1B6F-4CD3-AB76-FAB0875A2C61%40cmu.edu.