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 27498 invoked from network); 14 Apr 2022 01:28:43 -0000 Received: from mail-lf1-x13f.google.com (2a00:1450:4864:20::13f) by inbox.vuxu.org with ESMTPUTF8; 14 Apr 2022 01:28:43 -0000 Received: by mail-lf1-x13f.google.com with SMTP id bp19-20020a056512159300b0046bac0601a3sf1683851lfb.1 for ; Wed, 13 Apr 2022 18:28:43 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1649899722; cv=pass; d=google.com; s=arc-20160816; b=L4LDkT6b6GTtmycBFV+cPNwM9YfO0dUrEE/XkdMS0sZqJKnoE5LgUJbWS/NjGWydpN O0i212bS9vxhqvGROf5KHov91eayLY/GlT4yULKVOQWSPBUZs+HQBqCwbgUqS5tzOtW+ XhUinNDocM22zZ8S4ClXIoAmNZui6Nsb1NNT8z1bGL8dtZp6R0FgOvXR9Fk+UnDlmIwe LENwEhkL9MlUhiQfbG7BhRHIYMScOFeRQ9Ig7sqDmOyV5T9rJulAnsIsSIqdgm5D549i SvkElUwDKKEfFQ8FsJ2eP4dnXaeG5cPkiBqzUZnQZgccZbskvDBoF7i3TXfvXfF9ucpO cdGw== 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:in-reply-to:references:mime-version :sender:dkim-signature:dkim-signature; bh=ta57oYh7y4HNnVNtjaZIhJ0Qvvp/yd8G2dTStu989ys=; b=ZVS2+U0cJIyc6XUkNQKoBseKv81AdZmZDbYmHmcWKYzE71uQRmiCYlz/hoWYVa7y79 mbRI+pgpcL3iq0hdDHS3jBy8YnTRXzJjlw6Ymul7XnZ7amvSBmJg6d+oflleYvDB/9JC SjPhMj0tkvJSHE2stT5NwtKMDDPaa1cOu2Vv7zP0eJQiaUxbyvDiqP3B4xZGSy8/uPIg 9xL4kSGYrIkUFqX8Vlj37RwAoX0wH3WJ6UquhZ3V6bdeTE2+hpSEeFPxsXHPbAM56kNS nGJcOVT5pbspbL7212HMktmvhrNw2+fIPgW2VEfQMhB9ZfqRwESa/6YePw68HNE1Sr9b 7t+Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Wt+tr+Ub; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::335 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:references:in-reply-to: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=ta57oYh7y4HNnVNtjaZIhJ0Qvvp/yd8G2dTStu989ys=; b=siNaeMre7QH1gldw2TlWn4sjaNpQHiRHMbW4xXoOYliXEPuriCaJupxHsdXOq2XEim q6UmrFmHjKEkqQmzLajIxIdFhIF/DFDLNELzVKeGkIiA7XsoM8Zl3X87Wyw+j0D37L3Q ed3fXtpj3BS38f0bRYAxsumZEqNJiEScNknS0EJb6HhgkCPm0qw+bb1HXZYGNd7gy1xn QRprgM3YixBiIE2VjknklGxIH96cvZqNDlyu/sMo1BOfvA+IqZBBYZvwDRnI5y4udky8 NXIexg43FYNspO9VFw3Ut9k/7355vrlMbwMorC+cN9vFuIM8awVk9hsuAKHyx3pX1NZh 6vcQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:references:in-reply-to: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=ta57oYh7y4HNnVNtjaZIhJ0Qvvp/yd8G2dTStu989ys=; b=a4hqVjeew3HUlPVcrkSeoxvKRXtRE7FLIgh2E8ySKl7oSFgOwqVw4CwUIE8iWjcugW N6iTRYC4C2NZxuc+FPJC5Ht3mU32M0QY2nnpbTiK9h6yFOAxWJpALiwSQCKDDS7zOKfl M1YLgrjJ2MAxAzJ8Z0Vwju82cMuS7NgZwbX3s334xfoZXe7+DVlmng6hH2W/4Y255yds gE2K42cOLQ1/IkoRwshaNXdaMhgH2EDTMxUnNWdD3cnFOO+RZJxf5cUZVkrQs2lzUvgQ b/+XHVP8BwACUddE7f75JeFwUmZMdw9GOhdfcffs8yR5dHp3SI9tMaHMHrW64D9fUb61 tA0A== 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:references:in-reply-to: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=ta57oYh7y4HNnVNtjaZIhJ0Qvvp/yd8G2dTStu989ys=; b=sS3SJEy9C1kioY6iJMmjZCMrWuid+ZmBvNGsdbdbd6yVqLGDAy6Onm8AUzcRJ5QQU6 9RgAGhEajsMi0QgSo8O0pV6zLClSZ9Rz2uZHCZtP4wYu3leeFHt1t5OBZAN+v5tdym5X Vs40AfNW6R9cahWWiGIec8yrZYWQemNjEeHGk8rHeDWDrjxf9ZYEPHy3spIfY//KGPY8 nKgBBpppKc+0GNexfMejVBEvv1/MUjWccyabiLl/CFxMn0OSTm1gjBu8y99B5t/wkJEn nEovAM0mYVyA9GBcEYrcxd63w2+NwgQJagnPYPUcIjjUFdMooTA/aWBAssOqoAX8PO3N mqcg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531mNJoXXzd1+jO04Du/YG9VEf9IkxWqgPeS2GBTH9x82vq88/wP A/o/bLzbpbvteq+ZPcwB3oI= X-Google-Smtp-Source: ABdhPJw3GvIwfvUlG8jeZATPn61UJEvWpwg2wasTl68ksuSV7vYHQ0dNWkeVsbzzBDyPBAVQg6QZqQ== X-Received: by 2002:a2e:a448:0:b0:24c:8fe8:f3c6 with SMTP id v8-20020a2ea448000000b0024c8fe8f3c6mr220566ljn.115.1649899722416; Wed, 13 Apr 2022 18:28:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:5285:0:b0:44a:94d2:1d8f with SMTP id q5-20020ac25285000000b0044a94d21d8fls3348827lfm.0.gmail; Wed, 13 Apr 2022 18:28:39 -0700 (PDT) X-Received: by 2002:ac2:5f4d:0:b0:43e:da3e:4529 with SMTP id 13-20020ac25f4d000000b0043eda3e4529mr294997lfz.627.1649899719831; Wed, 13 Apr 2022 18:28:39 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1649899719; cv=none; d=google.com; s=arc-20160816; b=zqW9EkmZoF8fmc+8c+GUeIdgNZfPxLA3Q6yl1oJa1HnYdMTbFg/sYBcZKtxlOEPffT Z+XoZ8ZkQ0uaw1hiQqbQo1Z2TeZKFm51/Eu259w4hC8z30/s8yUQXgrliBvVboT2TZ5x JD3nTjKDBjmSadoenBHtDPx/EhsIIlzqVD1P6LRBKL7ce6Q3jm5+2LmRyseE6DNV8hHa 2QJBhi6TgYR10HAkphFBkDaG+9CEYvFZd5WM9MRHQ72Wm7ulR8sJ5duzcD/xfNBt2Pf/ hXwQEHTWCvYZ4WEEEuaPwxPcE5I4cJD6gAirAl16pZCWREq0NNocY0rgimETjQZAlaPD SDww== 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 :in-reply-to:references:mime-version:dkim-signature; bh=RkLB1Auqm2+uDphfOT0ju6bgn76LEnFw8vOheBCVMBo=; b=WpD9Esq0eElYQbbe6VzGNmZSrH2C1s5YhVy93gTBEyztUQqjquHQS7V2CjSCh4siMf FNOrQDZgIuk72vUMkmGG1MH6tTuAG+8YC6UJQ0GTZOziQx6KgBvR7sSQn5bma8s/bL4K /DNi/NasjT3CLLCnbbVrNWEXCa+9n2CRE6UUl3lJnz52rn3c6Sc+wZkJkJwyqRjI4FFZ XwCviueJj01a1nxOdVqbm+gsiyH1b+X6TeOnIjLQqv2R54f9BoajNUMqW1WGscrZY9Q5 74opNEWnHjkZsdMoD5UGpoMe0i98NMOxGsgFctM8WE0TBXh/SQv8OH0yiwWJqT6HxRGq F6SQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Wt+tr+Ub; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=k.kapulkin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x335.google.com (mail-wm1-x335.google.com. [2a00:1450:4864:20::335]) by gmr-mx.google.com with ESMTPS id c9-20020a19e349000000b0045dda698a90si246712lfk.1.2022.04.13.18.28.39 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 13 Apr 2022 18:28:39 -0700 (PDT) Received-SPF: pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) client-ip=2a00:1450:4864:20::335; Received: by mail-wm1-x335.google.com with SMTP id q20so2133852wmq.1; Wed, 13 Apr 2022 18:28:39 -0700 (PDT) X-Received: by 2002:a7b:c30e:0:b0:37f:a63d:3d1f with SMTP id k14-20020a7bc30e000000b0037fa63d3d1fmr725607wmj.178.1649899719135; Wed, 13 Apr 2022 18:28:39 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Chris Kapulkin Date: Wed, 13 Apr 2022 21:28:28 -0400 Message-ID: Subject: [HoTT] Re: 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=Wt+tr+Ub; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::335 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: , The organizers of the HoTT Electronic Seminar Talks are committed to the diversity and growth of homotopy type theory, and want everybody to feel comfortable and welcome in our community. We believe the speaker=E2=80=99s recent statements in the context of the Ho= TT Book stand in opposition to these values, and have made the difficult decision not to hold the upcoming HoTTEST Distinguished Lecture Series. Carlo Angiuli Dan Christensen Chris Kapulkin On Mon, Apr 11, 2022 at 9:32 AM Chris Kapulkin wrote= : > > 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 h= ave > 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/CAEXhy3Pjt4%3Dwi5ikinGTqkKXyQKQ6iWOCtyTjz%3DBc1zufLz-AQ%= 40mail.gmail.com.