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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 10727 invoked from network); 22 Feb 2023 15:31:29 -0000 Received: from mail-qv1-xf3e.google.com (2607:f8b0:4864:20::f3e) by inbox.vuxu.org with ESMTPUTF8; 22 Feb 2023 15:31:29 -0000 Received: by mail-qv1-xf3e.google.com with SMTP id pv11-20020ad4548b000000b0056e96f4fd64sf3742787qvb.15 for ; Wed, 22 Feb 2023 07:31:29 -0800 (PST) ARC-Seal: i=3; a=rsa-sha256; t=1677079887; cv=pass; d=google.com; s=arc-20160816; b=RTC0w83DthItsqFSoxw8Xtf9GphbC7JQgC0Xng4JovgydVW2X9CQ6A/Dae0iHPKCar /My2SCQzOa5PFparZRBB71MW6E3hLbAmgMFgrjd5CzFZC5z40nVU5oD/wk3XiISx7MUf Xstoqkltu1K8xjqBD3XWQf6yjhOn/59+TzIDt/am6rN9PuF8SsccRIyOCCWyrB5bnSGF tWEJsTkaib+ft1IwXGElm+cKRRWchPWRhm9PRR0J1eWn7WA3H/90G/8GgJAUuPU/YZyI GWXn5J/s5Bm04K7X0CC+0k3l7MnjN5Rm1eNykdWHpT7OM8tSpBOoMGUKAyx0uWrgpsmJ D9Sw== 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-language:accept-language:message-id:date:thread-index :thread-topic:subject:to:from:ironport-hdrordr:ironport-data :ironport-phdr:ironport-sdr:dkim-signature; bh=/siwxCeVuWdLDjaZZTjYd4j2seVXUwBblnssTLzSMnk=; b=hrmPdRyddNB9JxmRD1ZhkwSvY84BAtyLZ1ZAQGOKRp6nHRMj+XQpLNXPYHOThMdDAA xQMCYBOM82UYjx9nUfqbj51sl6G0RrC0H2LgqlcMbTensRFf3MmFYXoS29/Abz5R8NnU ci7OsCWAnnembj6rtD08SN7hzvWBYclE1Wr2KuCq8jZAkwdfs0fKvcLplZ2taIWFWvj6 0AXNZwnTWaMRQMF7dxSb8xo2Mjt2wHLtdHfUbwiDH/Oj7meuagIwwHAk3+qFnyR3oavo Gct9po6MbWkGqDAQ3sQjC38NXerGU67HtrSlhbaeMUrQigH/x/DK7tTeOgJQLhzrh1pi sU1w== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=IgIGSBrb; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=VuWhyrCp; 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=410a3ca44=eriehl@jhu.edu designates 128.220.39.150 as permitted sender) smtp.mailfrom="prvs=410a3ca44=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-language:accept-language:message-id:date:thread-index :thread-topic:subject:to:from:ironport-hdrordr:ironport-data :ironport-phdr:ironport-sdr:from:to:cc:subject:date:message-id :reply-to; bh=/siwxCeVuWdLDjaZZTjYd4j2seVXUwBblnssTLzSMnk=; b=aZEompqCFWpfXAe7TU9nsV/3u5XZseg9WO21D80yYnMdkMQ0tLUR+X6SCdrYJDvGTq KkVGu+Dw6NLnNDrcVkCYcLZZy4UbOjk8i6YvYyEPpR+4zpwNAKPjcSeSYXAYbjvzvHrB ikofDKyD6TEhyxQWhF69ECZyryoIk7rbk552shq0d9mav/k3K+/52IXdwkjP1YopfLmL 2UWviqJ7piv/f6coteJl17izVZClm6YHFvVfgbgBe8HMl3fNRnhX1ISReRQK2QzDMGo8 7IiTAukNHpAHTvynvALepwiISWjEUGfkNWTjR4aETHtCr+Mc2fH4hGfLANkZyaJkFZ0h izog== 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-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:subject :date:message-id:reply-to; bh=/siwxCeVuWdLDjaZZTjYd4j2seVXUwBblnssTLzSMnk=; b=zOCaJeBDUSkNl8IC03/gbmnu7BeGL5agzohXaINDZa090OzNzPz63JaRGhAijY2+Nz i+a5g6IvvsMnpJZ9UAxOE3SpBTvSCsPw+izsAYNVtx5ArJkeQR2VflXkEVmO+7OTejSS fTGPiR1HKeKZVZFQyhKKqgNVSCM4udRUx+q4Vujiz1jctbruB7uHKKkcmCF9VcRrCyEE KDRkJzN+VYsgoZ/XXUaeASrc6teIKOHCVFt0/jIaZ9fQshhrk3f394pu1FHo9SWmN034 g96m6pcyj8djhTgBQon1JwkTwswakJhzsNFdw24kHC2z7mxUhLjrw35Psv6OQLhbScw5 7DhQ== X-Gm-Message-State: AO0yUKVd/Niz3NhPwE3WTprxs8SocPN5LpPWXKsUbu50MmSWsc4Tby1v aSO9xQUlA+qcG44qeGlIIDA= X-Google-Smtp-Source: AK7set9E+VKe3t2teQjgXkXTU2W2fjxThaI1d9a11pIB/wlP/oLdHetu2iZC/ltRCPAXeF7TYg+arw== X-Received: by 2002:a0c:a950:0:b0:572:744:36e with SMTP id z16-20020a0ca950000000b005720744036emr457080qva.72.1677079887065; Wed, 22 Feb 2023 07:31:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:48d5:0:b0:3b0:98a4:96b8 with SMTP id l21-20020ac848d5000000b003b098a496b8ls6559251qtr.8.-pod-prod-gmail; Wed, 22 Feb 2023 07:31:25 -0800 (PST) X-Received: by 2002:a05:622a:189b:b0:3b8:525f:f0a7 with SMTP id v27-20020a05622a189b00b003b8525ff0a7mr27375896qtc.56.1677079885615; Wed, 22 Feb 2023 07:31:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1677079885; cv=pass; d=google.com; s=arc-20160816; b=qhVY/7Z2bWF2NFBXX6zhomMYmgJH1jhxMv1JFAGUiUbPP4ORh9S83uY9EiKe6KJXh3 hSH4PuzluBqjTQPZWTVT4rEE2NZNe/w9Uhggp2QOByxNvBgnePPyVTJQrOyzyBmvWygN rTq7Gq7vlrUMZEwgkB1xYkFalTxTt/wuvTsxuBdAyqrs0TzLi/ekZaYeZV2lttSz/MV5 oTxcKHtoo0zZS+RBmTDDHpwe3ULqFM2eCDMfgmhjQlwYw5R+yHNwG7yBIKIE7QrEobkE UPiYBPEnLkgEDpWDhky4jjAZPSVj0cRt4+Ou/kBQq5lvTpfvRGMvkr9qZ6XEkB3dPc4l Yjig== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version: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=3OgEO7Tqetn1mWCWCxSKhx1eS/2K4eFVHWz28mKU/oI=; b=P7q471AUdzjCyKzXvqauXar62HAMB1dfj5P9O5LsWF4KnbMIdIwhv2nkgWfEla9YdV AiuFN+p+PHzHQs2BT3/iYqYG/cZn8hImYTYFI+OlbSNyYlcRlbclZa3AO0i26/P77QW4 NO/QE4lwrACsAqVKuPYWNegwpQnUKXsRRHJsDOwh48eJV8eAclcR/bpzSDMVil43lAC5 k8IbCKGD1qcwWIKr6DyiKIvgZc+Kc5nQyTfUybZxBxcCU/JiLUY2fZGexGWkRsojQpbh UNP7xl202Z7SMQYIDhEGRinl44gA/thFdwIeXS5jaXimW8TBJyj/WCQlZ6d/tXLaDPaA /dwQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=IgIGSBrb; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=VuWhyrCp; 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=410a3ca44=eriehl@jhu.edu designates 128.220.39.150 as permitted sender) smtp.mailfrom="prvs=410a3ca44=eriehl@jhu.edu"; dmarc=pass (p=REJECT sp=REJECT dis=NONE) header.from=jhu.edu Received: from IronMTW5.johnshopkins.edu (ironmtw5.johnshopkins.edu. [128.220.39.150]) by gmr-mx.google.com with ESMTPS id z8-20020a05622a124800b003bb820fca79si519031qtx.1.2023.02.22.07.31.25 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Wed, 22 Feb 2023 07:31:25 -0800 (PST) Received-SPF: pass (google.com: domain of prvs=410a3ca44=eriehl@jhu.edu designates 128.220.39.150 as permitted sender) client-ip=128.220.39.150; IronPort-SDR: BAG4+NVw6ddo87Tv6Y/poavVQR1fYk49B+lPLwpTaRoGtjhyStO+hebjKc5o8iXNPiYRxhvqtp kTIvwRUFpmoFetz55s65yrJCNbI6LbF7hmPVGSwZA2R55cd+CDHTjWitAnasdHnOZxCJMFKGll UuDAkEtGNtbrLKzfks4GFiUW8UeyIwjoLQt0p8Sufu+9tsaYaxvWv5jZwUO2cphjsEtgNIJcwy zIQ820EveILwPJWGxZBZiKZKrmDWfvJ3HyH5ascYSCmhPVr59zp4tjxRCZnX15QFw27aEXg1Pv JC5JrfYMHncRVxkCIzTtyzqb X-IPAS-Result: =?us-ascii?q?A2FYBABtNPZj/3yErQpagQmBT4EqgQOBBwKBWbINgSyBJ?= =?us-ascii?q?QMYFigGCQEBAQEBAQEBAQgBOQsEAQEDAQOEOUUChS4mNAkOAQIEAQEBAQMCA?= =?us-ascii?q?wEBAQEBAQMBAQEFAQEBAQEBBgMBAQECgSYNVw1dC4FEC4F0CwMxDYI3KQERZ?= =?us-ascii?q?E0GMwIBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEFAg0HS?= =?us-ascii?q?wcigRUBATgRAYEAJwQbgneCFlgDMRMGqzOBNIEBgggBAQYEBIE4AZsTGEYBC?= =?us-ascii?q?Q2BXgkJAYE2g0qFS4gYQoFJRIFYgjdugQWBXQIBgWErg2SCLot6iW+BNHSBI?= =?us-ascii?q?w6BQoEJAgkCEXGBFghoXIEjBCYHNgNEHUADC3U+ATUUIwkkNVhEJAUDCxUqR?= =?us-ascii?q?wQINgUGTxECCA8SDyxEDkIhFjQTBnkNCw4RA081gRMEc4EcVZpEAlAhboEYo?= =?us-ascii?q?FOiJQ8xg1CLYpUuFoVLo2mXVo1SmhwCBAIEBQIWNYEtghZyEzuCZwkKPAECA?= =?us-ascii?q?QEBDQIBAQEDAQIBAQEJAQEBAY4ngxRUgmSFHYxWdTsCBwEKAQEDCQGKbwEB?= IronPort-PHdr: A9a23:Y7/phRcpNrs4tiAeYNv3wBLFlGM+sNnLVj580XLHo4xHfqnrxZn+J kuXvawr0AWUG9yEurkb16L/iOPJZy8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T 4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglWhDexe65+I ReyoAnetMQbjpZpJ7osxBfOvnZHdONayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU 7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4 ql3RBP0jioMKiU0+3/LhMNukK1boQqhpx1hzI7SfIGVL+d1cqfEcd8HWWZNQsNdWipcCY2+c oQPFfIMM+ZGoYfgu1sAoxiwChWjC+700DBEmmP60Lcm3+g9EQzL2hErEdIUsHTTqdX4LKgcX +e2wqfOzzrIcu9Y1zTy5obKdB4qvPaBUqxqccrQ10YvFwfFg06SqYzlIjOZzPoCvHWG7+d5U ++klmEopR1rrDe12scslpfGhpgTyl3c9Ch0wps4KMC2RUN1f9KpHpVeuiOYOoZ2XM4vX2Nlt ik4x7EapZK2czUGxYgnyhDQZfKKfZWF7xLhWeuNPDp2i3Roc6+xiRa19Eiv0Oz8Vs+s3VdLq SpFldzMumoQ1xzI8sSHV/V8/kC71TmTzQ/e7PxPL0MslafDNpIt3qQ8mocRvEnNBCP6hUv7g LGMekk55OSl5Pzrbqvnq5OAOYJ5jxzyPrg1lcG+BOk1MQ0DUmqG9um50bDu/Ev0S6hQgPIsi KnWqpXaKNwepq6+HgBazJ4u6w26Dze6yNQYmmQHLE5ddBKHkYfpP1bOLej3A/miglqilylly PDJMLLgH5nAL2HPnKnucLpn5U9cyQwzwcpF6J1JEL0BIvLzWlLruNPGExA5LhS4w+fhCNpjy oMTQX+DDrODPK/Ps1KF6PgjL/SCaYMLojrxNuYp6vH2gX88g1AdfK2p3ZUNaHC/G/RrO1uWY WDtgtgfEWcKuhEzTO7qiF2fSzJceWu9X78k6jE9E42pFZ3DSZy1gLydwCe7GYVban1eBlCWD Xjob5mEW+sLaC+KIMFhlTkEVb+9S48mzRGvtBH0yrp/LuXK5CMYtYzs1N9v5+zTjhwy+jt0D 8OS02GJUW50kXkIRzgr3KBnukxx0EuM0a99g68QKdsGx/RMVRs9LY+U8/1iBpjOWg/GZMbBH HahR9K6BikgcsMpzuMObkFnCv2tiRfM2yelGbgIj6fND5sxpPHyxX/0cutY6lL3nJMAonkCC p9CL2yrhqpX9QjOQYPFjhPKxO6Raa0A0XuVpy+4xm2UsRQdCVYoOU2NdXwcZ06Dq9P/6wuCS rK1Er0oP0NHztLKMapFbNDlzDAkDPfuMdjTeSS9zmG3AxvbyraFdoG/fWIb0W3UA1QFlAZG+ 3GAOEA+Cy6trniYAiZpEAftY16q/OVj+xuG IronPort-Data: A9a23:BY+AKKhWFYpMc8Lvr2yflf4ZX161lhAKZh0ujC45NGQN5FlHY01je htvWmvSPveONjH3Ktl1b9ux9k4D6pXXy4VnG1Q/qS48Ri8W8JqUDtmwEBz9bniYRiHhoOCLz O1FM4Wdc5pkJpP4jk3wWlQ0hSQkvU2wqz6V5NfsYkidfyc9IMsaoU8lyrFRbrJA24DjWFvX4 4mq+aUzBXf8s9JKGjNEg068gE431BjCkGtwUosWP6gjUPf2zhH5PbpHTU2DByKQrrp8R4ZWc 93+IISRpQs1yT92U4/4zeyrGqE9auW60QCm0hK6UkU56/RIjnRaPq0TbJLwZarL4tkgch8YJ Nhl7PSNpQkV0qLku78meiRlKnxFIrQa06fCcGqW4d685hiTG5fs660G4EAeELY339pILFEXq 7lCdHYSbxbFju7wwrKmDORgm6zPLuGyZMVG5SomlGqDS698HfgvQI2TjTNc9Doqh81OGd7cZ 9dfZDZyBPjFS0ERYQdLUcxuw49EgFHQQT1ornmLnZM62G/C0w8pl6TyC5nsL4niqcJ92xzwS nj910T+BxYGM8SO9Sud/06si+jVjAv0X4UdELC37Pl3mEbVzWsWYCD6TnO2uva8llGzS4sBb hZIvDUvq+47+AqpTsS7UhGlyJKZgiMhtxNrO7VSwGmwJmD8vG5130AIEWxMbsIIrsgzSWB43 1OFhYq1VzF1sbCVTVqf9qrSoD+vYHBHIWgHbC4CbA0E/9i6/t5v0kKQHoY4Hf7nlMDxFBHx3 yuO8Ho0iYIV3JwC2KiM9Fzahy6h+8rSRQkv6wSJAm+ot1srZIOsa4Gyx0Lc6PJMcNSQQlWb5 SRWltKf4eAKJZONiWqATPhUROOl4POMMTv9h19zHsB/qGjxqyHzLdtduWgsKl1oP8AIfS7ST HXS4Q4BtoVOOHaKbLNsZ97jAcody/myHNvoYfnYc95Sb8UjbwSA5ixvOxKd0m2xwkghlaYzZ cWSfcq2VyZIJJ9I6QaJatdEj/pxmmYhxGWVTJy9zRS6l7eSeSfNG7sCNVKPaME/7b+F+VuKr 4oPaJvakBgPAvfjZiT38JIIKQxYJ3YMA8GkosNaQeePPw56FTxzEPTW274gJdBokvgHjOvO5 X3hCEZUxECl1S/KMgqPdm9ueOqxGMwj6206O2olMRCq22VlbIqytf9Ne5wydLgh1epi0f8tE aZZJ5XfUqQUR2SV4SkZYLn8sJdmKEahizWIbnisbzUIdpJ9QxDEp43/dQz1+ShQUie6uKPSe VF7Ot83nHbbezlfMQ== IronPort-HdrOrdr: A9a23:Mzp+J6nFt1JzK/JwZYtS6HMHLULpDfOkimdD5ihNYBxZY6Wkfp +V88jzhCWZtN9OYhwdcIi7SdG9qADnhOVICOgqTP+ftWzd1ldAQ7sSi7cKrweQeBEWldQtnp uIEZIOceEYZGIS5a2RgWmF+r4bsZy6GcuT9ILjJgJWPGZXgtZbnmNE42igYy9LbTgDIaB8OI uX58JBqTblU28QdN6HCn4MWPWGj8HXlbr9CCR2TSIP2U2rt3eF+bT6Gx+X0lM1SDVU24ov9m DDjkjQ+rijifem0RXRvlWjoqi+2eGRhuerNvb8xPT9GQ+cyzpAo74RG4FqiQpF791HLmxa0+ Uk7S1QffiboEmhBF1d6SGdpjUIlgxer0MKgGXo/UfLsIj3Qik3BNFGgp8cehzF61A4tNU5y6 5T2XmF3qAnei8osR6NkuQgbSsa4nacsD4ni6oennZfWYwRZPtYqpEe5lpcFNMFEDjh4I4qHe FyBIWEjcwmOG+yfjTcpC1i0dasVnM8ElOPRVUDoNWc13xTkGpix0UVycQDljML9Y47SZND++ PYW54Y4o1mX4sTd+ZwFe0BScy4BijERg/NKnubJRD9GKQOKxv22uzKCPlf3pDbRHXJ9upApH 3saiIoiYdpQTOQNSSn5uw0zizw X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.97,319,1669093200"; d="scan'208,217";a="463841687" X-Amp-Result: SKIPPED(no attachment in message) X-Amp-File-Uploaded: False X-MessageIPDirection: Outgoing Received: from esgmtwex16-24.win.ad.jhu.edu ([10.173.132.124]) by IronMTW5.johnshopkins.edu with ESMTP/TLS/AES256-GCM-SHA384; 22 Feb 2023 10:31:22 -0500 Received: from ESGMTWEX16-23.win.ad.jhu.edu (10.173.132.123) by ESGMTWEX16-24.win.ad.jhu.edu (10.173.132.124) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2507.21; Wed, 22 Feb 2023 10:31:20 -0500 Received: from NAM02-DM3-obe.outbound.protection.outlook.com (128.220.36.245) 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.21 via Frontend Transport; Wed, 22 Feb 2023 10:31:20 -0500 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=UqSlOSnxNB72pVrWTRaD/R+gqzZ9zabjHbYmkp21Y5mDw0jQCAGqjXVpE99iEPcEJz7wfzcvBBjyqhq7nnMNFumlJDvuclr+Mv9jNkCYVzSsUfu+0QS6vz5ljr8gQ07rugcgkougzhA7pOZsMOjEeF4N4nLGPeR2yPn8pAOOqg8rXouLaqRPrp+UGRsOYe5Hmbb1Kh4bNp+kuJeW8dbjXE6RUkZyAYIQN4eut1CLDrlQI7yYyVLzy7pypJ9P3y4Wod8W6EyeA3sDtbHMqB4jovRdxJSyBpjS9HtdHbtPlI6JReFGLlS9QmF0ftZvYUaTNnJdKEAhnfMktzGt0bRKww== 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=3OgEO7Tqetn1mWCWCxSKhx1eS/2K4eFVHWz28mKU/oI=; b=AbYMISglbB4r6jZsvl1d2t55vqT2rUofSx9askrafjUSvcSI4lfso23oyiMch6CISuVuBFPaa3a20wtHtkgXdFi3YyDFUKElrw0jWE7fwgkjhcWKypVBfbn4IwOP3XrpWDlweBKElq650k0DcF8gBdxstNB/DaObO0FAh0ySiQFbO+9oLgW2vrtv6zFNjtwB5ILRc18d/ZVc1zcuTpZD8k2Vj2eHLtfohvowhdU4NV8k8HRGSGf0LodeSVfv+sqE+4WxavYXB6ChSrq/d/GZ4XM82wdRfrkXm4MIQJGW2Ui/C98jYOhwum1y3TdvPfKohFt6SMZ+v+WytNUsirPVBA== 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 BL1PR01MB7722.prod.exchangelabs.com (2603:10b6:208:396::18) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6134.19; Wed, 22 Feb 2023 15:31:18 +0000 Received: from DS7PR01MB7758.prod.exchangelabs.com ([fe80::4f97:4d46:688b:363a]) by DS7PR01MB7758.prod.exchangelabs.com ([fe80::4f97:4d46:688b:363a%4]) with mapi id 15.20.6111.019; Wed, 22 Feb 2023 15:31:18 +0000 From: "'EMILY RIEHL' via Homotopy Type Theory" To: Homotopy Type Theory Subject: =?UTF-8?Q?=5BHoTT=5D_February_23=3A_Lo=C3=AFc_Pujet=2C_Observational_Type_?= =?UTF-8?Q?Theory_meets_CIC?= Thread-Topic: =?Windows-1252?Q?February_23:_Lo=EFc_Pujet,_Observational_Type_Theory_mee?= =?Windows-1252?Q?ts_CIC?= Thread-Index: AQHZRtJrvYkIOkQGskWyZVhhyM3g+A== Date: Wed, 22 Feb 2023 15:31:18 +0000 Message-ID: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-publictraffictype: Email x-ms-traffictypediagnostic: DS7PR01MB7758:EE_|BL1PR01MB7722:EE_ x-ms-office365-filtering-correlation-id: bb31b6cf-7470-477b-2d84-08db14e9d7d4 x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: K6qEcQOszyZ9sDj9RrpbnlJ7mZUdl1aEnphxH1wVI4kFbpE3r2FgxVhUQFEgTUdgKXXVeRXu7c2P22Q2SEuBiQQJqEnBmQsKddhSWvNke8TqroxKBS8nwxBwgfrNwW/9GApWfLuFMcoAUNtmWyQ4BJ6CddG21bm+dQEkOWvXriYWrgXxdI8zor4mbfXbx6zPWyOF2sFsgniAg0BYJYXZwwACkz+G8lxYkwnLGqhfamTL38eUOU2ZQNkYhLER8m1bPd1xEqra9vl5gt/WFT10FeQGZwxNX2m0WbvU+cgHTX+YqARJZbA7P1+shK3jWptQCvH5FwgU++DIIt3v+s6AbDUIAvDWi0/2D1h9eb8OLiyUhi+pHjVoMrxkfKcIJD6pA4ywv5T3XDxR4AJBu85B4LJf2PC9XNdU2Rd0BCguvWh/mG63hShfUxokDJ56jqAPpC7/8JYLS+qUNeAKrelJKiRVL+wEYIhKMeFA/a3KIoBmAEcwODD25vwwyDgAyygLj84f5YDOR8ZoJZsMZaZen9cAJ+kPONSx+YL4cJt0oyw/G+4I0V4tre5VWRccT5VF/gUkWmktQskjf1qGWbYJNc9ETed3Reia9CS3bnXqrcnHIT6LnqluJPFMRKyXwceAt7PhxC3S6TmODftoQ2kn0v7GoYAp6Lxyt6LLWk9RL0mJyvCnhD2xdS9tjD/mPhLy 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:(13230025)(4636009)(136003)(396003)(39860400002)(346002)(366004)(376002)(451199018)(38100700002)(5660300002)(52536014)(8936002)(21615005)(2906002)(41300700001)(66574015)(966005)(7696005)(316002)(6916009)(186003)(66946007)(478600001)(64756008)(26005)(6506007)(66556008)(66476007)(76116006)(66446008)(91956017)(786003)(166002)(9686003)(71200400001)(33656002)(224303003)(55016003)(41320700001)(86362001)(75432002)(38070700005)(83380400001)(122000001);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?Windows-1252?Q?7SaWRUtaOgpOmqePHjkif/xFJOMBV8SnZIgxIqkDrYC5RrKzAOKa/9ZR?= =?Windows-1252?Q?JnZxXM+qItcDJQcajOOEG+g73cBVqo1H0UzdOp5IkO1WiZr/cxHIDcS7?= =?Windows-1252?Q?Ldt6LApmz5+QDG67z6sHHBmzDZSp7YAiPz71CwoCno/Hr6qxTfBO67p4?= =?Windows-1252?Q?RmHykVvxSW8/MAqU+Kvdlr6BGzCe/dJqGBKDroEvCMAm8IemFy9cu+A+?= =?Windows-1252?Q?8KIheYL9is/qwl3OgAq5f+4dGJ4UFRetAu8XqMY/odeObIqRxH7OKxMm?= =?Windows-1252?Q?N9aeNoZLvhy7ZUa7ic2lQEAY6sm+gFxB/aWdJm087OP/vpFY+gadjuIx?= =?Windows-1252?Q?kg6Dfgd2wWUkvTqAzhKvYE8WYbTHf1MMhQmWvvKygw+4bl4oXG6qrCb4?= =?Windows-1252?Q?Xxo8S9ogBn3iqqdubhlw33Gmq71pfgq9OcSTNIW+dsfgHtpY6nQLgSwr?= =?Windows-1252?Q?JCB8WJ2ru9zlhM2ip6C41JdMBn+EQaRQ/+fbQz0dalfnSewk8mPUpval?= =?Windows-1252?Q?7QYaGpX53w/8QGk2tJcZQp1MjO+uV5cksMfV3AbQoSlk5U87Bo/oQTKX?= =?Windows-1252?Q?L9igIFkecJwEWntmc8zwnnvvXPxUt7sZGrRAVc4HikesoJlIntbrkhk1?= =?Windows-1252?Q?8UToEd41qz/YcOP2LMjEstATJCd6HUAEwnN7ZgKUvjEVADZcBjIjefON?= =?Windows-1252?Q?wL+uKFigiLC9GnWBvhdJ+nc1tjEO1Reg+AVuohDVG65VqJxRjG/aGXOm?= =?Windows-1252?Q?IVCb4c2rUhnmktT3X5BD9vAX94ypF7dMGVmlLbM2xHmrwDSZO6jssFzo?= =?Windows-1252?Q?WRZlTG8jEMcmI7tR83ygUXRx0ZAp+P4i70Y1hfdPK9vusUXgNABrUVvt?= =?Windows-1252?Q?ongH4xxsQBf/yhThobeRc5J+b9FC207crTT584H/UH6L5XkuQ1xCM1AS?= =?Windows-1252?Q?NArr/PZLD7y2Nd7ZRJ/6Ymn+mWOUfMxn+8PDrdsyttKbooElFXtFZfsl?= =?Windows-1252?Q?77Mpyql42ZfkkVNKBD7qUfP/6XVJezVipZA3LxqUByC3vnEBVaTyFv2c?= =?Windows-1252?Q?zflyJwHD18CJ8TXX6tmlZiA9L6MpgfdH5P54dBL6lDJA1Cw2oXJH0pNi?= =?Windows-1252?Q?rvneOvqBinz8SjVROSfN1jbu2HSjFWj8yuoQU2pwx73u0cAg5bQZPbjr?= =?Windows-1252?Q?V81f87icGFoARJGGf/1calIkQUupd+YHKj+wz93CrIoSoPhd91DhCcKa?= =?Windows-1252?Q?pR4EKvgvuoPa7ozkZuRzmDTXGydJ3ef3VqKjMzuQci00be062/2HULC4?= =?Windows-1252?Q?b+QkU0c7y7wXXDPeo5OoCqW48VUJLl1vLvunv2h7l2A72WduGtRGJsCl?= =?Windows-1252?Q?mR9YjJtz4BpWbGgNTwidPXe2iztFi0r/Ud0QPw+2qLjTwQKIhB5wZDDY?= =?Windows-1252?Q?VPC6qg58YQbvDHwOvRG6sL10nHETlU1CpixTa6FfOhMtr5swTSLKh/83?= =?Windows-1252?Q?lB+Ss+Z+auYMK+48Ax8epZoFWaL5XVos2sc9lWAj9KsndgnTx6nyzBWe?= =?Windows-1252?Q?bFV6yZejloi6YIUpxZ9SezGK+Z17f+fxeDmfE/MazBa4XUzjAuGvevCZ?= =?Windows-1252?Q?nElMtw8c89aYugAY44A/ymS0E9OkobNfa27g62MZAFYJMHVjXMxRpUMe?= =?Windows-1252?Q?/40+i+cLToLQtkqAojGB4uUpLw2ZMefc?= Content-Type: multipart/alternative; boundary="_000_DS7PR01MB77586E3980E74CA744BE8E74C8AA9DS7PR01MB7758prod_" 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: bb31b6cf-7470-477b-2d84-08db14e9d7d4 X-MS-Exchange-CrossTenant-originalarrivaltime: 22 Feb 2023 15:31:18.3374 (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: g1yDYKi+Wfj8VC8xt9je0VFCAUiJ6chWD6T4Oigo+okZj+KtoUUra4cJdOI1d45z X-MS-Exchange-Transport-CrossTenantHeadersStamped: BL1PR01MB7722 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=IgIGSBrb; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=VuWhyrCp; 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=410a3ca44=eriehl@jhu.edu designates 128.220.39.150 as permitted sender) smtp.mailfrom="prvs=410a3ca44=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: , --_000_DS7PR01MB77586E3980E74CA744BE8E74C8AA9DS7PR01MB7758prod_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable The HoTTEST seminar continues this Thursday at the usual time, 11:30am EST = =3D 16:30 UTC. Our speaker is Lo=C3=AFc Pujet, who's talk is titled "Observational Type T= heory meets CIC". The talk will be 60 minutes long, followed by up to 30 minutes for questions. The abstract is below. The Zoom link is https://zoom.us/j/994874377 Further information, including the list of upcoming speakers, and videos an= d slides from past talks, is at: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html Emily (On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.) -- Observational Type Theory (OTT) extends dependent type theory with an equal= ity that satisfies extensionality principles for functions and propositions= , as well as quotient types. But unlike HoTT, the equality of OTT is a prop= osition that does not contain any higher structure. Thus, if HoTT is the la= nguage of infinity-groupoids, OTT is the language of propositions and sets. In this talk I will go over the integration of OTT with the Calculus of Ind= uctive Constructions=E2=80=94the theory of Coq=E2=80=94which supports both = impredicative propositions and a large class of inductive types. In order to obtain strong theoretical guarantees on our theory, I will expl= ain how to build several models for OTT: one the one hand, models in set th= eory to establish consistency; and on the other hand, reducibility models t= o establish normalization, a type-checking algorithm, and bounds on its pro= of-theoretic strength. Finally, I will discuss the use of OTT as an internal language for Grothend= ieck toposes and the principle of unique choice.This presentation is based = on joint work with Nicolas Tabareau. Most of the results that I will present have been formalized in Agda and Co= q. 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/DS7PR01MB77586E3980E74CA744BE8E74C8AA9%40DS7PR01MB7758.p= rod.exchangelabs.com. --_000_DS7PR01MB77586E3980E74CA744BE8E74C8AA9DS7PR01MB7758prod_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

The H= oTTEST seminar continues this Thursday at the usual time, 11:30am EST =3D 16:30 UTC.

Our speaker is  Lo=C3=AFc Pujet, who'= s talk is titled "Observational Type Theory meets CIC".  The talk will be 60 minutes long, followed by<= br> up to 30 minutes for questions.  The = abstract is below.

The Zoom link is htt= ps://zoom.us/j/994874377

Further information, including the list of= upcoming speakers, and videos and slides from past talks, is at:<= br>
https://www.uwo.ca/math/faculty/kapulkin/s= eminars/hottest.html

Emily

(On behalf of the HoTTEST organizers: Carl= o Angiuli, Dan Christensen,
Chris Kapulkin, and Emily Riehl.)

=  

--

Observational Type Theory (OTT) extends dependent type theory with an eq= uality that satisfies extensionality principles for functions and propositi= ons, as well as quotient types. But unlike HoTT, the equality of OTT is a p= roposition that does not contain any higher structure. Thus, if HoTT is the language of infinity-groupoids,= OTT is the language of propositions and sets. 

In this talk I will go over the integration of OTT with the Calculus of = Inductive Constructions=E2=80=94the theory of Coq=E2=80=94which supports bo= th impredicative propositions and a large class of inductive types. 

In order to obtain strong theoretical guarantees on our theory, I will e= xplain how to build several models for OTT: one the one hand, models in set= theory to establish consistency; and on the other hand, reducibility model= s to establish normalization, a type-checking algorithm, and bounds on its proof-theoretic strength. =

Finally, I will discuss the use of OTT as an internal language for Groth= endieck toposes and the principle of unique choice.This presentation is bas= ed on joint work with Nicolas Tabareau. 

Most of the results that I will present have been formalized in Agda and= Coq.

 

 

Professor of Math= ematics (she/her)

Johns Hopkins Uni= versity

emilyriehl.github= .io

 =

 

--
You received this message because you are subscribed to the Google Groups &= quot;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 htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/DS7PR01MB77586E3980E74CA7= 44BE8E74C8AA9%40DS7PR01MB7758.prod.exchangelabs.com.
--_000_DS7PR01MB77586E3980E74CA744BE8E74C8AA9DS7PR01MB7758prod_--