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 autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 3131 invoked from network); 27 May 2021 15:48:17 -0000 Received: from mail-qt1-x83a.google.com (2607:f8b0:4864:20::83a) by inbox.vuxu.org with ESMTPUTF8; 27 May 2021 15:48:17 -0000 Received: by mail-qt1-x83a.google.com with SMTP id v13-20020ac8578d0000b02901e4f5d48831sf366624qta.14 for ; Thu, 27 May 2021 08:48:17 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1622130495; cv=pass; d=google.com; s=arc-20160816; b=IQIp+VHms0QQ1ZdSF7KGFSQcpXyI+qQ4+KUY8go9KwPM25wlb9AsBcd2ipLixgY9XB u2GEUS5AM0vh8DAFk21nXwRbsMTPATAz+bHRJF0DvSrFcXtJZzBOK0TVJKdV+DD/YIO9 2c40pXmSRo7uPLzDN12Vsa0gl7JJiQNplFYuzfAVjeSojGEJjytilmvMjAGGDDWk5BPi 47Va1R38YuHJwd70AQQEXfAolKvQURGkmlfPIDVcEPb+wp618PExXayhrqiiUMniFHgU 22ZbKGIPeTO9HLIjaDBGAVat4IYaSgwVbX/NRwmBgPIQGjDPMDXS1Z5VVBdSAnou0+53 3uXw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe: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=ueYXFk5ynzsh0lZc3/uHM8FmYm5efUd6u7bmCDYobZo=; b=uEUfTbsIGqA1M7I6r1QfGse8gArQni2wNzVr/vylgcDu72dX2cp+xYYOMCmGK3kF05 45aqMxif9X2kPNGgwSYiU4CSYq8QGBCV0GfL1dVtbqXGXCJMrsozmEri4jwVTHUvz5f1 XK5n5EhgAkqCZPP7PA0/QbrBxF+bHY/ome6tPonJLL/fQKl1vBMUNXpq/cM0OO10TJVO raUdj9kUQptors0Q4QFThWDyiJLXZt7smF3S11FH4reBwo80m/3oLkOr4e4Qp9Grxmez hpqSNOD3Vh7saahMiHP/ppM2H0givy+K3CO56dV8Hl1QqgC++//kSLqqgibTy1XeCkIj OSLA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="1wfPSDj/"; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72a 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=20161025; 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-unsubscribe; bh=ueYXFk5ynzsh0lZc3/uHM8FmYm5efUd6u7bmCDYobZo=; b=qOR7NGJbLMPzCpECt5FArxlBKqXOjMeeZx3lHYavHHlqNzTlrnbqKaQj3M1z9CuY1I JhaZwHrUDrzPewrC6HfXr4bDjFpdM0nYhivaq/IgcJKAgBlm9jkBtKkVADbb1btexlL9 5g5ryImvMWDeMwxyaG5nvb/b0VHNP1Di0+Nm4Qbi5rcE3QLtvdU3RrnOjLkr6lDf/8Z2 GGK/rNRZreKNsvlJroDOvLfoaYtoOXHeJZkdrIOW6AHSmq0C/w9AY9cgEWVDu4Ur9PQR XfO0nYPIHb0BXZzi/wEb9ReKB9Zo37YYIeVu6NEkpy5NGyadx2WctsquP1xTF+9H+bVM uCWg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; 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-unsubscribe; bh=ueYXFk5ynzsh0lZc3/uHM8FmYm5efUd6u7bmCDYobZo=; b=GxleSTcq+1bgpSGh3h1VxAGeQADiUn/n4VWG1l0SMwV5evV6S8yNXVC7hrKuLUenqO YtTnx9jhBpqZLm+W0LCZAUOfTHhAMMcEnQatsUF5JlMdIJrK9uq5uAiq4pRRSap6UvQq OdWQUSTlmFa7a1XYYAKtpbEJTFlL7MuHkvFXaZN23G9qRXOXqXMEmBPzE1lFE0WO7ecK P2OkxxFibwkTmKl2FADepqp5ahIBg9YgTUaob32r5kylvIkl+xKAC5TSwLrwCTNdbVer /3EI+B6npk/l1UO9w+sWAWf5Ry5rkhmF1f+s4c2FY0eCeDKT+rEdWLfJ6ONTOD/XOLlI vG9Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531Gus3UHU63rkJP412xbp9U9xRYs3ePCkvW9btX/wfkd8ENeFJ+ K+TfETBlnoBDvVI7vaT7k6U= X-Google-Smtp-Source: ABdhPJyXz0VuoAbvgOR7vvfqBpqireL+d6UZqfRzA5rmfhvPOuddP5bVmyG4u2oI7OPBQoVEi8zyPQ== X-Received: by 2002:a05:620a:4486:: with SMTP id x6mr4145789qkp.229.1622130495139; Thu, 27 May 2021 08:48:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:72cd:: with SMTP id o13ls1711634qtp.0.gmail; Thu, 27 May 2021 08:48:14 -0700 (PDT) X-Received: by 2002:ac8:6a1a:: with SMTP id t26mr3632106qtr.361.1622130494535; Thu, 27 May 2021 08:48:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1622130494; cv=none; d=google.com; s=arc-20160816; b=GwhIOTKf6NMCDC0MAh3WA0ychCfQ6w8f3wC0xMgI3I+Hl4JqJtKg8OY7LjUQ4IdRh2 XUFG4FbEQpqh8f+0hGRt0G5m8Y5EtNPqmUJPVX2wre+KQ3HO5PRtaQyJ6Y7J/QMHJBAb A1GEyESNv1b0iTU349V5bhSR0Rf/PXMEbCWrz2MI5P/LSlumG6vZlGWE12sJXKf1G4Rx zc9oqhX9ltlZTgdIrsFZwzFIjPwYArVQ9HNzpspbSMpozPr+5nj7qZ71VR1tmVVsjlFC MbHeOks4/9L6FylTLOq6Nm8c6cxgiMwcTnQeHTc+PG3Fj1DYIrjsBcHfNVDGkGkzekgo Zi9Q== 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=rE741/BQO01A3C7vF1C72cbv3JSc14O4ynWRTSUl97s=; b=gFRyWwzTisH3Nn0mFyWc6AA//GOaqqque6eq5RXzQN13OpDgw6bdq8Vx95k5/uQu/D dFt1JWY/nOuM+/cAbLyvCxHkow9ZYJzB2P/9zVL8IeQNqLX2diNcKz2xJGnmT4jlji9B QNJKXM/mRnzKJyuCyfynljSP6ITymHVfZvP/KLbAbsVZZHt87g6NWsVE4LJjxkFYkqOz K9GG2uIcYlaxW90hECmp8aQ1MNOZEwm7YQTFy1I5FTc/j/o23FEpywrzXApwfw9XmgNo 0HOpCDKW74KU9raGnHg6rHAEyXj54HS6jJKgjQ35niMLrU8Za2jrqe6J/R50BgWXBWxG OL5A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="1wfPSDj/"; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72a 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-x72a.google.com (mail-qk1-x72a.google.com. [2607:f8b0:4864:20::72a]) by gmr-mx.google.com with ESMTPS id a205si226486qkg.6.2021.05.27.08.48.14 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 27 May 2021 08:48:14 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72a as permitted sender) client-ip=2607:f8b0:4864:20::72a; Received: by mail-qk1-x72a.google.com with SMTP id c20so1089245qkm.3 for ; Thu, 27 May 2021 08:48:14 -0700 (PDT) X-Received: by 2002:a05:620a:2f9:: with SMTP id a25mr4068687qko.401.1622130493958; Thu, 27 May 2021 08:48:13 -0700 (PDT) Received: from [192.168.1.143] (pool-71-112-154-2.pitbpa.fios.verizon.net. [71.112.154.2]) by smtp.gmail.com with ESMTPSA id l14sm1571474qtj.26.2021.05.27.08.48.13 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 27 May 2021 08:48:13 -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 11.5 \(3445.9.7\)) Subject: [HoTT] Topos talk: Shulman Message-Id: <787184CD-C528-4D0A-9281-BD576C12C2C6@cmu.edu> Date: Thu, 27 May 2021 11:48:12 -0400 Cc: CMU HoTT To: Homotopy Type Theory X-Mailer: Apple Mail (2.3445.9.7) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b="1wfPSDj/"; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::72a 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: , ~ Topos Institute Colloquium ~ Michael Shulman: Two-dimensional semantics of homotopy type theory Abstract: The general higher-categorical semantics of homotopy type theory = involves (=E2=88=9E,1)-toposes and Quillen model categories. However, for m= any applications it suffices to consider (2,1)-toposes, which are reasonabl= y concrete categorical objects built out of ordinary groupoids. In this tal= k I'll describe how to interpret homotopy type theory in (2,1)-toposes, and= some of the applications we can get from such an interpretation. I will as= sume a little exposure to type theory, as in Dan Christensen's talk from Ap= ril, but no experience with higher toposes or homotopy theory. This talk wi= ll also serve as an introduction to some basic notions of Quillen model cat= egories. Time: May 27, 2021 05:00 PM Universal Time UTC (13:00 in PGH) Zoom: https://topos-institute.zoom.us/j/5344862882?pwd=3DZnh3UlUrek41T3RLQX= JVRVNkM3Ewdz09 Meeting ID: 534 486 2882 Passcode: 65537 --=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/787184CD-C528-4D0A-9281-BD576C12C2C6%40cmu.edu.