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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 14133 invoked from network); 22 Aug 2022 02:54:41 -0000 Received: from mail-pj1-x103a.google.com (2607:f8b0:4864:20::103a) by inbox.vuxu.org with ESMTPUTF8; 22 Aug 2022 02:54:41 -0000 Received: by mail-pj1-x103a.google.com with SMTP id u5-20020a17090a1d4500b001fad7c5f685sf4713009pju.9 for ; Sun, 21 Aug 2022 19:54:41 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1661136880; cv=pass; d=google.com; s=arc-20160816; b=0FkN8auN1haQdLHwKxnVxaO5sJ+fqc349Ac/wxOIPzUrhOazihvpwgHs2R61zJMuK3 5HzGnG79QJf95ddL2XUF6S6RNUfMwHcY/RB0nKC4vndz95PqE5zH96zDY2081WE0pVYa oLWz9CTbi/YcawWDnB9LLFv5KjpUaPA4Ay+EHaOQZSLdRmKqo347sYyELeFaibzaLFRh SmeMxz/JSIaqYy6xv6kubJFqI5A+8kmSdEssNvalZuHne1WC3CPdNhjxLuqDKfo5EQJi 9uHFK5A2/vHPpZMn9Vf1PdChiDKhHQECN2tyLrIrMWFdX3vHsL44/5K+bz7fLO8ihvpL 6aYg== ARC-Message-Signature: i=3; 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:reply-to:mime-version :content-transfer-encoding:msip_labels:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:ironport-hdrordr:ironport-data:ironport-phdr:ironport-sdr :dkim-signature; bh=lvimmNe3VXMwQ669IsywRH5gOhfEdPBaw7B+lxnKjBs=; b=r9ZXBOyOCf/GPAYNbtgM0MsZTsikI1Y2sU3+cP2sczRRUETe0WVmV9pvUV4An7sXKq M+o4r0p1ZnWBHepkgMXEMu+rAqqNHdAva6aaPeDhQds4cE4yycDsOc+QhubhaqJqhnAI uw1HSh4tnVcEoB558JluMIsRjIQS3T7cSns4TUrxksxMRnzUFJqTx4qgIG4afLPiQVi9 xvj1OiaBv8374aOIyM89mGzWtETIpJeJ6hElXmUKVLk8tSRvINp0MlYLua4zOpTxvC3Y JU7fk2U6zlAYpPyawC70KBQ9BnSclOeM3WDROcG6ezsJpFAiAryRRz1Jg2Vbrmg8HiAo JJZA== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=Msb+HJFz; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=CS0e1k+P; arc=pass (i=1 spf=pass spfdomain=jhu.edu dkim=pass dkdomain=jhu.edu dmarc=pass fromdomain=jhu.edu); spf=pass (google.com: domain of prvs=2263f49ec=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) smtp.mailfrom="prvs=2263f49ec=eriehl@jhu.edu"; dmarc=pass (p=REJECT sp=REJECT dis=NONE) header.from=jhu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender:mime-version :content-transfer-encoding:msip_labels:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:ironport-hdrordr:ironport-data:ironport-phdr:ironport-sdr :from:to:cc; bh=lvimmNe3VXMwQ669IsywRH5gOhfEdPBaw7B+lxnKjBs=; b=HTEgmBQKWRgw1WlIPAEIr8eIf2kRRODGcA0rubvc/7QY6eVYjitKO9OFlBm0V+v4N6 E93B9etgD5ZvJrjjOeUAFMd4s5Y8KiNkKikKIAiVRjriVKIoDJNRfJgCVCyc8rfPF+fN qLjKCW2RCIGc2ToqzerQ7IlulQE8VwRSTssqa8+s++izIM1MgryAWaWKrBQ2HYLlViSE LlYx7BPoS7mWRLEDQZQolTJXD2fPE1LkoztzDEd89wa5+iz7DErrOrTX1J2MQYeeaNKZ 71HTQwrgo+ubNOHdmPRD8TNi1gO68ryYJ/B1chvzoeLgp/8Bk/xYtDC7J1XYfZEBdchW 4fMQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender:mime-version :content-transfer-encoding:msip_labels:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:ironport-hdrordr:ironport-data:ironport-phdr:ironport-sdr :x-gm-message-state:from:to:cc; bh=lvimmNe3VXMwQ669IsywRH5gOhfEdPBaw7B+lxnKjBs=; b=olSiMUHLl9JNOOM+u+kEkkmoQgpRwQ75LqkTFz+MPOiktaJoeM1FTtDMszxJANH0vn M9fGJXv8O/zLM4NuMs7GbRCU1I7QFHFwPbFgZUqqbYfnxelf6sXYfcSiRNRhcPmFls2N GdnIZxxyTHQocgC0iPYdo5dlf3Iv/bLifEZ1WwWlxOBHAlPhoKxQb1rPPcxCdCkVF323 XgKV0GN7ODWXwhLR+rEFJrIuBYPXXP8JoLGQ312Z9NRUmcLbOjxMT2XsSIefTGt2Fw3G jzPW18qi9fWfWlGdhPrzHagSm9EuytG5VguXdwA18V5xuTjSwPmolaBXEWhdwQpLY7oR gs0g== X-Gm-Message-State: ACgBeo09KE+374Rf3gmTpKsdW1TAvNQB43v0um8prhErW6oJDz1ZNSRC 7utGDjvhAI9fWO0K1ZufLuo= X-Google-Smtp-Source: AA6agR6dhH65RUX7pEOuBqSlCeZfmmefN8faQ8KDTw2RC6E5G4jKbcyByUlpRzV1XXgLsbJ9D4Sesw== X-Received: by 2002:a17:90a:f8c4:b0:1fb:2f6b:12ec with SMTP id l4-20020a17090af8c400b001fb2f6b12ecmr2901441pjd.201.1661136879764; Sun, 21 Aug 2022 19:54:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:7e85:b0:16d:82eb:cc57 with SMTP id z5-20020a1709027e8500b0016d82ebcc57ls6828001pla.11.-pod-prod-gmail; Sun, 21 Aug 2022 19:54:38 -0700 (PDT) X-Received: by 2002:a17:903:1c8:b0:171:2ed3:6780 with SMTP id e8-20020a17090301c800b001712ed36780mr18662861plh.30.1661136878110; Sun, 21 Aug 2022 19:54:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1661136878; cv=pass; d=google.com; s=arc-20160816; b=QJ3xwlJ9Q9ziRPzkQnCdrwKT/QPHdqbZjxb5Cjrup7jRcZE2rdwMlDStlhHZSF8Gpq L7qlvsXnLpmH8hzMtRjLIjF9UQq1ETcxyitdVDyyPy4lWRnFcHYLo5rOyN7xUOEqiBHU 8XttyP3jc9569XhQE8zlU7ssSTzz0/ICv+jtXx4DXu37DddlLXGOilxgcytWXc/jUn5n tidQ98tOYGlW0Jt7yr8fx03lolZX2QwtLxB32ca4oCDL8GdfZGL8zZDVYu+Wii0rj3q4 tNFGZZ5/0SQwACI8wPcD2O/ucoBwpk8YDKi+7weWjnKycShaWXlRpu4lnbgEV3n205Bw cDDg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:msip_labels:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:dkim-signature:ironport-hdrordr:ironport-data:ironport-phdr :ironport-sdr:dkim-signature; bh=NFmFL4/hoHnCod1+dP3qfyxfMN4r6T5YGoFoFDKz3JU=; b=Zqovrd8+pw5IQr6WHookmWvqAD8Q6pf1XBqp5rxyVakY7RpjN4pLl4mPGLe+5x/GuN jNCojcuqZoUKjUAmd5gUMjKSg4A1OaLWFZvv9SbrOOlZ5NdUb7oOi9zZ/uAP7yhgvIps fRy+i9S9GQmRk1c561lWOrBhMO0aPcXB2FMCm7ZdppX1eIE1PM+GyCLXsBOc1VmZVm/B HsFXNZHqNG0Cx6WzMeGQmfRsCM4Xem5BkXiK/HfVkonWvtuAfC42cXMwTORBEV4nGKSU z9tgbr1qdDDh8Lh5oxzlGd/AJ990PCQTo59vpUEeHuYWor4mYsLOAnRX0NXt3jrV2m/7 2D1Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=Msb+HJFz; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=CS0e1k+P; arc=pass (i=1 spf=pass spfdomain=jhu.edu dkim=pass dkdomain=jhu.edu dmarc=pass fromdomain=jhu.edu); spf=pass (google.com: domain of prvs=2263f49ec=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) smtp.mailfrom="prvs=2263f49ec=eriehl@jhu.edu"; dmarc=pass (p=REJECT sp=REJECT dis=NONE) header.from=jhu.edu Received: from IronMTW6.johnshopkins.edu (ironmtw6.johnshopkins.edu. [128.220.39.160]) by gmr-mx.google.com with ESMTPS id l17-20020a170903121100b0016d5881a19dsi511057plh.2.2022.08.21.19.54.37 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sun, 21 Aug 2022 19:54:38 -0700 (PDT) Received-SPF: pass (google.com: domain of prvs=2263f49ec=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) client-ip=128.220.39.160; IronPort-SDR: gpelZL3dJWhuBavpCuGBnrNc7t3rNeIopOC5apjY0HSeV8YIr48qd5NqpwOS7VcwU9MUFSGbIU LlvvzIub98jNS4ucVlkRQ2y5fOYw6i2fuLDVccFOJaqIsalq89ma1tIEsdsfw8wtn6fwMk5P9r aOdai2wxz1dfGdB2b1whsY9AqOJ/fpVln+cdGQs+jjZ60evaDHK0nz/wk675N3qQ0KxO1EBT/I QWPkYi+FClFdr3tP3Z7RMqdVYyUOSj2sFkWw7/jLD+ZMQuKqZXREtIEb2PFrxF2D1CfkXXbAVP 6gRz94AEdmx9tQSshd2cwilt X-IPAS-Result: =?us-ascii?q?A2ESCABJ7wJj/4aErQpRCR0BATwBBQUBAgEJARWBUYE6A?= =?us-ascii?q?mZ/AoFZklmDAptaglEDGDwCCQEBAQEBAQEBAQgBEgIDDhILBAEBAwEDhQACh?= =?us-ascii?q?GMmOBMBAgQBAQEBAwIDAQEBAQEBAwEBAQUBAQEBAQEGAwEBAQKBMmRogU+Bd?= =?us-ascii?q?As0DYI1KRJjTQYDAS8CAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBA?= =?us-ascii?q?QEBAQEBBQINUilCQgEBOBEBPUMnBBuCdoJtAzITqBmBM4EBgggBAQYEBIE4A?= =?us-ascii?q?YNYGEUBCQ2BXAkJAYExAgEBgyaMLUOBSUSBWIF4hA8CAVtYLoQLgi6MeIxtO?= =?us-ascii?q?ANFHkIDC0gICRcSEBACBBEaCwYDFj0JAgQOA0AIDQMRBAMPGAkSCBAEBgMxD?= =?us-ascii?q?CULAxQMAQYDBgUDAQMbAxQDBSQHAxkPIw0NBB8MAwMFJQMCAhsHAgIDAgYVB?= =?us-ascii?q?QICTjkIBAgEKyMPBQIHLwUELwIeBAUGEQgCCA4CBgQEBAQVAhAIAgcBJwgPB?= =?us-ascii?q?xMzGQEFCk8QCSEcKBAFBhMDCxVtBUUPKDM1OSsVCBsKgRIqKRUDBAQDAgYTA?= =?us-ascii?q?wMgAhAuMQMUBikTEi0HK3UJAgMiawMDBCgsAwkiHAcJIiY9BQVbPwMDECI9B?= =?us-ascii?q?gMJAwInmSyCCIEeIVArVoEmA5IZAY9ijBmRJoFkDzCDLIsrlRUWg3aBUJFjk?= =?us-ascii?q?UuXB404mX4CBAIEBQIWgXiBf3ITgyIJCjsBAgECDQIBAgMBAgECCQEBApIPg?= =?us-ascii?q?mSFHYJddQI5AgYLAQEDCYpcAQE?= IronPort-PHdr: A9a23:9xcAzhBuXSD1CNtKC+u0UyQUh0QY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua82ygWXA86FsLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G 9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys9ZDfeRtEiTu8bL99L Ri7oxjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3T bpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58 axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7Ses4URXdaXsZJSSNOHp+8Y YUID+oEJ+lYro/9rEYKoRaxAQSgAeXiwSJKiHDrx603y+QvHx/b0gw8EdwAs2jbotr6O6oJT eC11bXEwSnfY/9KxDvw7pXDfBA7ofGLWLJ9acXfx04sGQ3DjFqbtJDrMTCa2OoPtWaQ8u1tW vy1i24mtQ5xojyvy9wuionJm4IZ0E7L+jhkwIssI9CzVUF0b8K+HpRKqyGaK5V5QtkkQ2xwt is31L4LtYKncCUI1Jkr2QPSZ+CGfoSU4h/uVOmfLzl6iX57e7+ymxi//VWjx+D4S8S631lHo zRBn9fDtn4Ayhre4dWJRPt6+0euwzeP1wbL5+BFJkA0kq/bJ4Q8wr4rjpYTvkXDHjP2mEXrl 6CabEQk+u+u5u/6YbvmvoeRO5Johg3kL6gjmMKyDf4lPgUAQWSX4/mw2bPs8EHhXrlHj+E6n 6fcvZzHOcgUva+0DgpW34sm6RuwEjKr3dEZkHQBMVlLYgiIj5LzNFHLOP34CPC/jEmynzpz3 PDGO6HhAo3KLnjejLftZbZ95FBYyAo01d1R6I9aBLAGLvztWkD/u93XAgI4PgCtzevqB89x1 40fWWKJGKOWKr7dvUWK5uIvPumAfpEatyvgK/Q95v7ui2E2mUMFcKW0wZcbcm20E/ZoLkmDf HbhjMkNHX0XsgcwQ+HmkFiCXiRSZ3a2UaI8/DY7CIe+AIjdXICtgaKO3Ce/HpBNZGBGCk2MH W32eIqZRvcAcCSSLdR5nTweSbehU5Mh1Q2ptALi1rZrNvDU9TEAtZL/yNh14PXemxM19TxxC MSdz2aNT3l0n20WRz42xL5wr1J9ylid1qh4mfxZGMdc5/NOVQc6OprcwPJ1C9DoXQLBY8+JS E28Ttq6BjExS4F5/9hbQ0F4HMmllgGL4zuyDvcpl7GMHo18poLb2n/tIN5s92fe2ZUhgl48U +NAMmqpgqNw7Q/OH5WPmEKcwfWEb6MZiQPo1UOyhVCvkWF8GFp9S6TIXXQ3ZEvL69n1+xWRH PeVFb07P14Zmoa5IaxQZ4is0AwurL/LNNffZje3nGG9TVaNy6iXZYXnM2MawG3GCUcCngxSm BTONQU3Ciq75W6LCjtoGAHjZkr2+rx4r3W2BkY/0wCNaRhn0Ly4sh4YjPCRUbUdxLUB7SUht nN5EEvut+8= IronPort-Data: A9a23:ls4oLKnZMGqi1qG1fhtScrDo5gxHJkRdPkR7XQ2eYbSJt1+Wr1Gzt xJOXGzTaK6CZmLxKIxzPoi280MCsMPdmNc1TgZtry43ES4T+ZvOCP2ndUqhZCn6wu8v7q5Ex 55HNoSfdpBcolv0/ErF3m3J8CEUOZllwtMQMcacUsxLbVYMpBwJ1FQywIbVvqYy2YLjW1PX4 4uryyHiEAbNNwBcYzJ8B52r9UsHUMTa4Fv0aXRkPZinFHeH/5UkJMp3yZOZdhMUcaENdgKOf Nsv+Znilo/v10x0Vo76yOaTnnoiGdY+NSDW4pZftjPLbhJq/kTe2Y5jXBYQhNs+Z5xkULmdx f0U3aFcRzvFMYX+uMg0eBwBARpcPJQe6r2aPUqClcuqmhiun3vEm52CDWkbBqI9xtlaMTgQs KdEbi8MaFaKi6S0wK/9R+Vx7ighBJCzetpA4Tc5lmufVK16KXzAa/yiCdtw0S0xi8BKNfTee owUZScHgBHoP0YeZglPWcxi9AuurnTySBZXlRXJnI8U32+I1wJu/LrPbPOAL7RmQu0QxC50v Fnu32P8BQ0dLM2j2CKIznKhgfXetSz8X40WGbKi8eNymxuYwWl7NfENfVagrvyllUOuAowac BBS5Sso66E+sk6rU5/wUwDQTGO4gyPwkuF4S4USgDxhAIKNi+pALmRbHDNHdvI8s8o6GW4j2 lOTxo+7CCZuvb2RYXCd6/GZoS7rYXoZKmoLZCklSwoZ4oS/+9hq1k6XFtszQrSoitDVGC3rx 2zYpiYJgbhO39UA0L+2/Ayajj/1/srJQwc56x/5RGWg6g8lNoepa5bxtQrW9/dNLIKxTFmc+ nUIhpHGvuwJCJiMkg2LQfkMQe3yvq/dbGWEjAc2TZc79jmr93qyRqxq4WlzdBVzL8IJWT71e 0uP6wlf05leYSmxZqhtboPtVsknwPSyFdnhUfyIPNNCboIrJF2qxw5LWXG97zmz1RNw174+P 9GSfYCuDWtcBKh6lWLkS+AY2L4t5yY/2WKOGcuilkz7ieKTNCyPVLMIEFqSdeRlvqmKlwPYr oREPMyQxhQDDeDzPnvN/YgIIQxYJHQ3H8qm+cFMeeufPQd2QT9kUKOX3rInPYVp2aZVi6HF8 mzkAh1Uz1/2hHvmLwSWay0/M+q2Bcon9X9rbzYxOVuI2mQ4Zdr95qkocZZqL6Is8/ZuzKIpQ vQIEyla7i+jltgaF+whUKTA IronPort-HdrOrdr: A9a23:UR1S5KrjdLfopN9tPtOfCgoaV5ulL9V00zEX/kB9WHVpm5Oj+P xGzc526farslsssSkb6Ki90dq7MAjhHPlOkMIs1NaZLUHbUQ6TQr2KgrGSpQEIdxeOldK1tp 0QOZSWaueAdGSS5PySiGLTcrYdKbG8geSVbIzlvhJQpHRRGsZdBnBCe2Km+yNNNWt7LKt8MK DZyttMpjKmd3hSRN+8HGM5U+/KoMCOvI76YDYdbiRXpTWmvHeN0vrXAhKY1hARX3dk2rE561 XIlAT/++GKr+y78BnBzGXehq4m1OcJi+EzS/BkuPJlawkEuTzYJLiJnIfy/wzdldvfpmrCVu O84SvIcf4Drk85NVvF2ycFkzOQrQrGrUWSjmNwyEGT3vAQSF8BerZ8rJMcfR3D50U6utZglK pNwmKCrpJSSQjNhSLn+rHzJmZXf2eP0A8feNQo/ghieJpbbKUUoZ0U/UtTHptFFCXm6Jo/GO 0rCM3H/v5ZfV6Tcnic5wBUsZWRd2V2Gg3DTlkJu8ST3TQTlHdlz1EAzMhamnsb7poyR5RN+u yBOKV1k7NFSNMQcMtGdZE8aNryDnaITQPHMWqUL1iiHKYbO2jVo5qy+7kx7PHCQu178HLzou WzbLp1jx9CR6u1M7zx4HRiyGG8fFmA X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,254,1654574400"; d="scan'208";a="439460964" X-Amp-Result: SKIPPED(no attachment in message) X-Amp-File-Uploaded: False X-MessageIPDirection: Outgoing Received: from esgmtwex16-34.win.ad.jhu.edu ([10.173.132.134]) by IronMTW6.johnshopkins.edu with ESMTP/TLS/AES256-GCM-SHA384; 21 Aug 2022 22:54:36 -0400 Received: from ESGMTWEX16-23.win.ad.jhu.edu (10.173.132.123) by ESGMTWEX16-34.win.ad.jhu.edu (10.173.132.134) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2507.12; Sun, 21 Aug 2022 22:54:35 -0400 Received: from NAM02-SN1-obe.outbound.protection.outlook.com (128.220.36.247) by ESGMTWEX16-23.win.ad.jhu.edu (10.173.132.123) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2507.12 via Frontend Transport; Sun, 21 Aug 2022 22:54:35 -0400 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=RuMV+m9Ok0Q/6EoBZ7UkztN5FRGQu9aWCuCPDpvkKmxsEmz55JWMCVBYb+BVOhX/Zk/s8JXVfsm4rPHKyu1VZm9wl+Xu/57gx45wHt0ercKechDEPdR/sXd7wqdRWhmtQIosBCfmdqTHihK/giowTdLn49cLKvH2qG7dlM/JRnyeJeUirWVCTMi4qYDPNiHTmnWqVxKcnCs2yYRnpnk5o0++wR1pk7fB+MWgnED451NcyC+cJhxGFCcprlZNP0Zzji4sJUv0+cNm8dB5wy93mXGe0V2a4OVQWn6YxRnGSnj4NcY3hjFY9C6/ZEqcAoaK589Xfm7hjXH4inZx7lwQMg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=NFmFL4/hoHnCod1+dP3qfyxfMN4r6T5YGoFoFDKz3JU=; b=J+YlABjEjqu20MzQXsUe1ayJDf+vhuTvEe5eEQgsRz5oMfkATEiMCByF0eG+md5M+GmarEy1a57WqB2A9o2DLL4UX9qxU1+TJDiE6P0W2e9nQmVYtaa+F/VDYrPtmcHvKTJsHW9iSSIIrcMwLDto9rWbBxlcP/tX9SlMoCw4kt3kMOMi89aSlR2D3dvNA905/AjxqpcEvdKaoiegGLPO/nkGrPxPRAlH1WyKbKuKecTWB8CGHwWhfpR1/TWeQFZxtFXGUa38chWw++YkwyW7NFDiQQSBwDd9wWp3RnrnKs+g6X8aYbnqjJkjETpaFWx1UFp9ma6U5CyeXMOdCyOmZw== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=jhu.edu; dmarc=pass action=none header.from=jhu.edu; dkim=pass header.d=jhu.edu; arc=none Received: from DS7PR01MB7758.prod.exchangelabs.com (2603:10b6:8:7d::6) by SN6PR01MB4223.prod.exchangelabs.com (2603:10b6:805:a5::20) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5546.21; Mon, 22 Aug 2022 02:54:33 +0000 Received: from DS7PR01MB7758.prod.exchangelabs.com ([fe80::ad14:1e97:8eca:65d2]) by DS7PR01MB7758.prod.exchangelabs.com ([fe80::ad14:1e97:8eca:65d2%6]) with mapi id 15.20.5546.021; Mon, 22 Aug 2022 02:54:33 +0000 From: "'EMILY RIEHL' via Homotopy Type Theory" To: Homotopy Type Theory Subject: [HoTT] HoTTEST summer school colloquia Thread-Topic: HoTTEST summer school colloquia Thread-Index: AQHYtdFUUWGTmujho0WmJesHIcl/ug== Date: Mon, 22 Aug 2022 02:54:33 +0000 Message-ID: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: msip_labels: x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 5c7abe8f-8dce-464e-7ae1-08da83e9a466 x-ms-traffictypediagnostic: SN6PR01MB4223:EE_ x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: MbwFpapbnJMXdNDZmNopFYBVTz12fmoUfOKf+FSeLgxQju1q/7UC0ilPpiO9hEQnML/ybRmUWyooTJi7TCyrbs9HDt/4nUoaPTH63OSiReddf3kFdRONmMxfHf3JnQqIBRd6E68UqqUwK4WvLzJx4gmo2YJFg2mykhCd19R5ED6pVuDIxE37zX74qro9sopJPIzm67271OWv0cTTYehFCG1rFA/rNB0dwdiLIfr4ldiGe5TyY5rV/DjdrZ6JLJmRlrhUvo/4Y3IRRTQKJiKy4rMDngMXTock85eIoFgqiKrWa0S/CiV/X7r5z5bbrAnBTJjM6ExdEtuP8idjtCb9ZxFkQPNzBWzg8YyEA12wKUj36LxQ/bu0Yd2n1pr31RDjR8gaOddgqg15Y11ABJjd8BsbUco58IAVhazBhp9RwHaaixWPZADl8vDEXIu4fUfBFT2QD+Lkymt1gVy91tC0Yjj/zq3RppHU4SxPIrIQ+F5nmrKCGIV/SRqytgH1STZNw+0vPYBr4VhLr5C874NnP+nZKjr9J5tUflM440vjCr3VMT2Cd6mE7j99DRoCkQKVLvwsEx1kAEH/VnvHYnPRpGNaCIrEE2Bwdg9h95dQdNFcv3i/I/oKZ4dT0vF23o2JI8TxzY0CvM1wLzj5As1Qc+eBBaayg8BT2tMzE2JpngZV69Mq5QWbLSCYuo2C1q6y16wHwdFZsYtqKCCUfVSdDfac2t36P0FoLCacAzj806vkR4/Ol75fvFN3ySXjh1LvYtCABJNdX1p/2FOZJ+KxMILAc4SYe465m2AkHwSUMm8= x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:DS7PR01MB7758.prod.exchangelabs.com;PTR:;CAT:NONE;SFS:(13230016)(4636009)(376002)(136003)(346002)(39860400002)(366004)(396003)(122000001)(3480700007)(38070700005)(64756008)(75432002)(91956017)(66946007)(66556008)(66446008)(66476007)(8676002)(38100700002)(76116006)(26005)(6506007)(9686003)(7696005)(71200400001)(478600001)(41300700001)(966005)(52536014)(6916009)(316002)(786003)(186003)(83380400001)(86362001)(2906002)(5660300002)(41320700001)(8936002)(55016003)(33656002);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?iso-8859-1?Q?Go5PJQeRSGQJDSkBf85Uef4RV9ICU5qXAAVdjAmd2UVD4Y9DXcnDejJIqW?= =?iso-8859-1?Q?ZDNc8PfUMa+toj8BDlZfOcueVb4lCJmOfezM1nfdTE1+XTIfYo81ivMstU?= =?iso-8859-1?Q?f5/FfD5rj2h0ty/26fWDnXfOT2LBcEkprrUnFWyT0SuQ+JE6RWy3GwwINJ?= =?iso-8859-1?Q?thNxUtq4ECtoQduDiFeLMGA0FOaqbvKgZCju4fa4X8fYAWjNZhsIVA7bMw?= =?iso-8859-1?Q?LpCcdX1jyYL7nRSbb0JQHHVS0r3l7NAjKehJFTaAeyhJ6X+Fwmz2pZg811?= =?iso-8859-1?Q?+7NGy3C5smmKOui6wb0vA4Hsghe+iLa6cdi3qaD9tD4X5OoC9egFjp4X9I?= =?iso-8859-1?Q?xTQfnMGxarmei1fF2CR3cX4j+4z/Un8AWuuz8WudPfFzhjoPRKCLa448wq?= =?iso-8859-1?Q?X+9ObKEWdjY4Pskw1RdFWcf9mSCWp6b+iGMJgAx8/eLm8+SEHrVqXIUm6W?= =?iso-8859-1?Q?7sccQYT7uW+hTp6ApQheE2ltVHXzLxy9gUUmyxaAEAP5xRN7mJb3EXJBQi?= =?iso-8859-1?Q?Wwqzc7ZxctDNyXzJfMrdBVWAQBBMxhy378g60LtL4/Om8iwJaxRz4IbiPz?= =?iso-8859-1?Q?amWDNNb2sG5fPuVwJ/hkwSTUnyKZjdNsYwwvFq5bskiHjrvG5AqYX/SZ1p?= =?iso-8859-1?Q?xObfEJ2i3h8H1IZr8wfbKop++y4wpJu6RoNznTeHtyLiRUy5d2LG8WFMv5?= =?iso-8859-1?Q?j+yntzjDgo7G0Z6s2B6UPpA0Jn8ReB7HB87Z8ZZ7nz5fVXcMW6nAyTpZww?= =?iso-8859-1?Q?Ux/0XbnL8v9+Avi5a+SRCjC3fzf1IZRynJajZDKH2BXyJYrETYe4ueBhn+?= =?iso-8859-1?Q?j2RPgH9Fd9VcdKupdfAv35W3EAR8qK01l8AWC3i5UIqzJyENPX/R1sy8Of?= =?iso-8859-1?Q?3nscuNpKsoI5optB5kvS54L/lO4GoZZaUOt7uuNAIHmdUFJPNYuIHu6Ylj?= =?iso-8859-1?Q?ZLgz1zpBq1HA9SQGOv+hj4Iss1MjPv36ZYXJxpt6Lmj2Ee5pNQx0Lqt6bw?= =?iso-8859-1?Q?S/mc64MK3klrRx+xe1Ww9ujKMHvNmlVoeus1b8GwIjz/ZsNCuBBPe6o+5x?= =?iso-8859-1?Q?NS5t2hrksoLUS9InhTwccWF+hVqtZYFRI4V4d+H7/3WAb+P1oTdWAhUkHi?= =?iso-8859-1?Q?rATlT2sqoIczgiz+1sQ7xOIXKrcxhfQT+z8eJRWTlgKkIhms11Bv7GUype?= =?iso-8859-1?Q?ShEG6MkwOga6wSQraGxLrN8nBGsftkmINN/5bLSZHUsJlYzcr46CbSZIxO?= =?iso-8859-1?Q?KC4UElsZWJ1YWJp+WAmPnm+Ou+mbbmCZ7rzDVmXC9Ddx9Pofl/6WC0qFHm?= =?iso-8859-1?Q?NwZen6L4a0oMu5dzDmQ7jphY1QuZhPEGzsylvUvcY/A3nSB+dkV9u0Mq13?= =?iso-8859-1?Q?wnK83VC+DVmGMRUkcET9lPgM0rab0OW02KwOBLBf7djxSwqjyGYhhU1H0u?= =?iso-8859-1?Q?xBlylczl7On2OQae1V1KCapzka8IViO5pOYuDXa98NQg1YvX8j+1QW2eDu?= =?iso-8859-1?Q?myBtWPI83bsBs780l/jSB7bsmRydJpBQnuDdgjcBiaQQOld4soou9UtIqn?= =?iso-8859-1?Q?QIx7/JGqWH6LbVKxjbwkA5gYVnudAYBVbVxienYVQpQ1H68aReLPSeVmRm?= =?iso-8859-1?Q?hpRdPfk4L3rPQ=3D?= Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: DS7PR01MB7758.prod.exchangelabs.com X-MS-Exchange-CrossTenant-Network-Message-Id: 5c7abe8f-8dce-464e-7ae1-08da83e9a466 X-MS-Exchange-CrossTenant-originalarrivaltime: 22 Aug 2022 02:54:33.4519 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 9fa4f438-b1e6-473b-803f-86f8aedf0dec X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: af4Ou9jhkMJjqhiukUidxvo7HfggcWgImP39iWWZbTY53mwNRw1CS5+5GJVFurXa X-MS-Exchange-Transport-CrossTenantHeadersStamped: SN6PR01MB4223 X-OriginatorOrg: jhu.edu X-Original-Sender: eriehl@jhu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=Msb+HJFz; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=CS0e1k+P; arc=pass (i=1 spf=pass spfdomain=jhu.edu dkim=pass dkdomain=jhu.edu dmarc=pass fromdomain=jhu.edu); spf=pass (google.com: domain of prvs=2263f49ec=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) smtp.mailfrom="prvs=2263f49ec=eriehl@jhu.edu"; dmarc=pass (p=REJECT sp=REJECT dis=NONE) header.from=jhu.edu X-Original-From: EMILY RIEHL Reply-To: EMILY RIEHL 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: , This week and next, we are looking forward to five colloquium talks that wi= ll conclude this summer's HoTTEST Summer School. The talks will take place = on Mondays, Wednesdays, and Fridays, starting tomorrow and concluding at th= e end of the month, from 2:30-4 PM UTC, at the following link: https://zoom.us/j/99263826765 All are welcome. Our speakers are Jon Sterling, Pierre Cagne, Jonas Frey, Favonia, and Chait= anya Leena Subramaniam. Titles and abstracts appear below. Hope to see you = there! Monday August 22: Jon Sterling, How to code your own type theory There is a considerable distance between the formal rules of type theory an= d the code that you must write in order to animate them as a running progra= m. In this colloquium, you will learn the basic techniques of type theoreti= c implementation in the OCaml programming language, including the represent= ation of syntax as well as type-directed conversion. Wednesday August 24: Pierre Cagne, Group theory without groups During the summer school, two key aspects of HoTT (and their cubical deriva= tives) have been put on display: identity types and univalent universes. In= this colloquium, we will take advantage of both these features of HoTT to = introduce what I like to call synthetic symmetry theory, which is essential= ly a univalent type-theoretic take on group theory. The usual presentation = of groups as sets structured by multiplication, inverse and neutral operati= ons is cast aside to the benefit of what are, in my opinion, the intended s= tars of the show: the mathematical objects on which groups act. This is a s= hift in perspective, that many group theorists probably implement at an inf= ormal level of reasoning, which is here taken seriously at a formal level. I will introduce basic notions of group theory through this lens. People in= the audience with no background whatsoever in classical group theory are i= nvited to consider this as an introduction to a new fun area of mathematics= , while those knowledgeable about group theory in its classical form are we= lcome to contrast what will be presented here with the classical theory. At= the end of the colloquium, both the former and the latter should be able, = and hopefully enticed, to read further about the subject in the work-in-pro= gress book Symmetry (https://unimath.github.io/SymmetryBook/book.pdf). Friday August 26: Jonas Frey, Modalities and Cohesive HoTT Motivated by the example of truncation levels, this talk will start out by = systematically introducing and discussing the notion of *modality* in HoTT,= mostly following [1]. In particular we will see characterizations of modal= ities and ways to construct them. The second part of the talk will give a b= rief introduction to the ideas of *cohesive* homotopy type theory, which is= an extension of homotopy type theory in which modalities play a central ro= le [2]. [1] Egbert Rijke, Michael Shulman, Bas Spitters. "Modalities in homotopy ty= pe theory." Logical Methods in Computer Science 16 (2020). [2] Michael Shulman, "Brouwer's fixed-point theorem in real-cohesive homoto= py type theory." Mathematical Structures in Computer Science 28.6 (2018): 8= 56-941. Monday August 29: Favonia, Cartesian cubical type theory We have multiple variants of cubical type theory different from what we hav= e seen in Cubical Agda. In the colloquium, I will introduce another main va= riant---Cartesian cubical type theory. Wednesday August 31: Chaitanya Leena Subramaniam, TBD --- Professor of Mathematics (she/her) Johns Hopkins University emilyriehl.github.io --=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/DS7PR01MB7758EDA9277BB98584EBF5EFC8719%40DS7PR01MB7758.p= rod.exchangelabs.com.