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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 4644 invoked from network); 11 Apr 2022 13:33:01 -0000 Received: from mail-ej1-x63f.google.com (2a00:1450:4864:20::63f) by inbox.vuxu.org with ESMTPUTF8; 11 Apr 2022 13:33:01 -0000 Received: by mail-ej1-x63f.google.com with SMTP id hs13-20020a1709073e8d00b006e892eb3e79sf986349ejc.11 for ; Mon, 11 Apr 2022 06:33:01 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1649683980; cv=pass; d=google.com; s=arc-20160816; b=01bsRYJdGDbg0BiZa82f6UlI5hS8Myt9DtndHiT8H68J08pay/8pgozVGVOUCyvuB0 WPlyGW6aly2ga8E02vgTtFRJKuJe91vdxM2/u6LMjtLO8/B833zB7Of9U+ACNI7P2Vse X2fWBVWAZcztfZ8s6SeX5xPzyRqXWVIHPcep7UF/LBB3ukpeqCu6OCk8OVJP5twhCetl sFPDHXs7K5X1tzHRuvTUN4Hgb1CaiDjaKnS2lYufj59dMO2YK6K5+UHJtQV+g3BTpnlR RhMLEjmnObLCqQwiaDn6tWUQANy6eh9mloBKZlVM89ltuT5G/pSuUgvCvCYgwvobyepA wFog== 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:content-transfer-encoding:to :subject:message-id:date:from:mime-version:sender:dkim-signature :dkim-signature; bh=w29ljK66niOf9uA7AkZCxdE9w6PFUEvx4JQKPp67ZPE=; b=vDQ/6K7LMBeGrZLDfC3YNYPQQZiEkz1R0ek6sbdPZKn9r/Ixt8pyTpYwqOtvrHGgxB NTqOQUfycnJHUtnzNv0QcC5xsD3g6pSSbHyO37yOVR93ZkOWAcrWsGbn+/0Wz+wy/Aox SGGlCFFDT1kgWnZ8R3n4FVaQkKTfnanNYjgpP7fOe2XzOh0VulaNtlIV2oXKfyM3hbXW XjImcg4jy+y7lQtInqrnYTpre81kUg2tv3nRqXpYWWA06hf3acrs0cNdVe48SsdaCqih op1aR199ZEFW6w7GSoqBETV6pS21DkAA76UnK2lSAV57T06m/UK9O19B4zhBkO15XBi1 CLdQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=JngukMYW; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) smtp.mailfrom=k.kapulkin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=w29ljK66niOf9uA7AkZCxdE9w6PFUEvx4JQKPp67ZPE=; b=RU0VHt/cAfYDM99VbeJQ521qI6y0FxyB7pMxH6uN1Hx1hrexKQp9pi4WqP0NxbSBE2 qbN2aES5o87+s1xbgpthJlhAGyidp8K465TKeCoz6Ga3pzuAwSej1n+iM0LkSCcLe7hz GGvEyqDthNHeV03FExw+c8dav7Q3sFzzJXXl6i8uFBG3YkByOxeM2Dkxii6+m8C2T+EF ZfRUQEPd/1abem2taDFDAzC1VGrgYLFspRWtuHAtiVjYr46a8oY4USBZ+YED6L2HbrmI VbOqFxnmLpa/txEQ/WpZ/STO2zdSRE2N7CsVFrgUHrIoR8W7qkt6eBhn9sgtx+qn1F/k UU5g== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=w29ljK66niOf9uA7AkZCxdE9w6PFUEvx4JQKPp67ZPE=; b=qnmxh2zxj+XWJL6xoUhyaVtQB11qlsNfguvdPDREgAQ+28gpQxDs+rErPDvEFbunHp DXLCRy7q/JRG1BBPi0KfPMKMn35CpJcdaBWbX8HrLn+mKKfyHzk02QPJWcFGSz+Noc2y ZqSGVFx7eh/7/dBSvRZSQJWrNsh3G7kmcnsq1YebH+qNvQ824J8PMoZXOLEQW0oITCBZ XAskNu8mDj9mOw5uEoBx7CFpHkrxuoPgBKVX2X2jIPD9tjVLAl0FhGGGTP7RCdMcUDcB 1CdWdmuYcqeOYIXgzjHnCkjD+zo3tF1BPaZOSiVoLSgLZBqZjA63QqzxivKjk8XUDW3W U1ww== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:content-transfer-encoding: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=w29ljK66niOf9uA7AkZCxdE9w6PFUEvx4JQKPp67ZPE=; b=WVlCPJvwnNFWeW/EQB8eKp0v0YzpElEMNVy6dbjLpMGlEri6WCQWtbnguAdHhbuWqE yFFW+BwqnhYk8be06zHhiz0/f9EQye4mG7R0gHIhlnqJFFx64/S217073akI8WHNg17t eOFeazvMyIEKHNAfhc68o+KAfLio15CBK4RIM5QePTEzXEq6SOkrYOS/l4szYJBAy3WQ NBX0QzmFyuYlBqjHklu2YMdxlgllYkDlbfMIuoPoXbRlXztIac6GA2KJaIP2Vfzshlj9 D/qUkVByMfOFiEb/ssO/un+upKDAxS83slJ+1swbXYdKX7it9EDZKMQoKWHbSXKxUN0q dp7Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530tT2qyzCWURE3ODpZw0bmKiTr3mkfllFmmp592TA12g8QWr6P8 9XSr2hXUjp7uMCKT0vNAVIM= X-Google-Smtp-Source: ABdhPJzi2GWUT4MOnLMaiSMHb42uunTWmoRMSsuMpKNGihGcmJSz9pDVLqWNjeoxw0JfCi3qyxvwKg== X-Received: by 2002:a17:907:9482:b0:6da:a24e:e767 with SMTP id dm2-20020a170907948200b006daa24ee767mr30220904ejc.479.1649683980663; Mon, 11 Apr 2022 06:33:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6402:5108:b0:41d:18d5:5462 with SMTP id m8-20020a056402510800b0041d18d55462ls2264612edd.0.gmail; Mon, 11 Apr 2022 06:32:58 -0700 (PDT) X-Received: by 2002:a05:6402:350b:b0:419:1c11:23ed with SMTP id b11-20020a056402350b00b004191c1123edmr33635059edd.8.1649683978656; Mon, 11 Apr 2022 06:32:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1649683978; cv=none; d=google.com; s=arc-20160816; b=Htn1K5M6wOad16Cux8lp7etgJ5pHR+6HZ7L+sWqhiqfNjkgGcIZDibr8VIdrpDJ5KJ GncVG19d7Uvd0u9g2pkxI/ez/3oVhBKpffmPfHJsh0auQehYVTUwGAAu8zUFUM0G2vgU t9Whjx8hVlV7QS87iC1a8K9Hc2cwGtpMV9fgxheEbBjW3sd803UCLYHR2/qLVXt++J96 1cqY9QgFGcz/Rdi5pwOHzob/V3Lr4SIuPLmKCRN857R9UAGutSGEm1yJCWTZZoQkk1yA dwBhTG7tQGOSOIrf6YQtSe/bBpTWmc3+1eyz9wd4Vc8Um4q6K7lkx9FEZ8vjMQN9vx0i UhFA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=q/+W1tPQ+4YTlln80Qmh2HCpQGA7trZOYaCRaDwkv64=; b=Xy99xqI6lUB58Dix77+deKlfHAd9TvEoWaqD4wLyJ1zZd0efYDUlRNiWKmXcOhJyZ6 EKoOOLNFe0VFJ7rMfpkn+9eHOqIj5b2nhJdpYuY7AQ7P1xVcZpbH4WNroiDtbGHegJmJ lGmwzhbf+fdFcahFTCQynTNSh5pYOTgv3qbHlbheDlYYoF02Qm/jExIARrfvaHnoqOSp ES4DLEm/UgqQWqr04YVLqr8mQfgFKCQ5Ps3RQ9nd0/f93aGbutFv7mZWMn4Yqeg97dUR 9YLbtqoJyS9TJ0ttyd5FznLAfrIf1nMZk78nRhfuYTVRXiDpzRvn1UQ9tqKhzk4NSiO0 dIxQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=JngukMYW; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) smtp.mailfrom=k.kapulkin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x429.google.com (mail-wr1-x429.google.com. [2a00:1450:4864:20::429]) by gmr-mx.google.com with ESMTPS id s5-20020a50dac5000000b00418ed2675a2si418131edj.3.2022.04.11.06.32.58 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 11 Apr 2022 06:32:58 -0700 (PDT) Received-SPF: pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) client-ip=2a00:1450:4864:20::429; Received: by mail-wr1-x429.google.com with SMTP id i20so9926329wrb.13; Mon, 11 Apr 2022 06:32:58 -0700 (PDT) X-Received: by 2002:a5d:528b:0:b0:203:d928:834c with SMTP id c11-20020a5d528b000000b00203d928834cmr25732925wrv.500.1649683978019; Mon, 11 Apr 2022 06:32:58 -0700 (PDT) MIME-Version: 1.0 From: Chris Kapulkin Date: Mon, 11 Apr 2022 09:32:47 -0400 Message-ID: Subject: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series To: HoTT Electronic Seminar Talks , Homotopy Type Theory , categories@mta.ca Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: k.kapulkin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=JngukMYW; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) smtp.mailfrom=k.kapulkin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , We are delighted to announce the inaugural HoTTEST Distinguished Lecture Series to be given by Mike Shulman (University of San Diego). The series consists of three lectures which will take place on April 14, 21, and 28 at 11:30 AM Eastern time. The Eastern time zone is now observing daylight saving time, making it UTC-04:00. Each lecture will be one-hour long and will be followed by a 30-minute discussion. The title and abstract are below. The Zoom link is https://zoom.us/j/994874377 Further information, including our Google Calendar and Youtube channel, is available at http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html We are looking forward to seeing many of you there! Best wishes, Carlo Angiuli Dan Christensen Chris Kapulkin * 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/CAEXhy3MVeK4auqO3MTkjn0JBO0XoqV8k-5RnS%3DOfi%3DVDQv15DA%= 40mail.gmail.com.