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,NICE_REPLY_A, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 20660 invoked from network); 23 Dec 2022 22:52:05 -0000 Received: from mail-ot1-x33b.google.com (2607:f8b0:4864:20::33b) by inbox.vuxu.org with ESMTPUTF8; 23 Dec 2022 22:52:05 -0000 Received: by mail-ot1-x33b.google.com with SMTP id f8-20020a9d7b48000000b0066f2d64da41sf3219182oto.12 for ; Fri, 23 Dec 2022 14:52:05 -0800 (PST) ARC-Seal: i=3; a=rsa-sha256; t=1671835922; cv=pass; d=google.com; s=arc-20160816; b=CS6uhmBumXyDXbNEcitUuSumEWfAw/3tAA40nlpe+ATlBS5iIbZJFPxXurjPRQmskF VnzKAzdD7J9lTbvjHYyBrIZeCHiE+YQDDlOYSkzMzJuDsnnZ2sBFeAsjkQ0QAWdbSKHV vWN659L+y1SkPJGUoFOLM6cVYvvUP7dFBSD23S2DvUnxTtH4Cgfyj31ah7nKQ1Zc01x1 FyW6HDFv36y9r3gzO6oxRwVCtmtHhCH5PfO249FA9bDrGZaI5COiJtyCrQXSz2o9t/O+ PkoBGx6n7SVlGNTiSwz6FBY0DUo8XKa7wJFj7cKu2ymZvpTCuGaOpKIOSa4tbaRep92h uyjQ== 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:content-id:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:ironport-hdrordr:ironport-data :ironport-phdr:ironport-sdr:dkim-signature; bh=EXbAV1lYLh1Os3a0pFXylggf0POUGA4DKghVkQBsXTM=; b=qoVNsAx/SrlHFDxvSs3Fljf2M4wAMkudd1eJVArOPJxut5RivHgt45AXWVVBiKkD/O LP0CnTGDDCNX0iUi3j+q03BdJnJ/BzsH7svgW8BwWgdiyW/3zCxLIuB5dO27OWLX8nYK kbyaIjsSjsQOZmwtg39MxfJVzAS2gsF8AIKr068G5nMrnAltFAYbsAJBdE0mYjhHfRFf tFfLEJmA9NB0NqeLfi7a3eLcBDAnZrBZIYNFtWZRy8sL0QZvez7bAZxhPxEpZiH3uhOU 4DsoHKU1d3ABcB8SB48ecyLFM1m+roJ6UXeNW4JiXzFBBh0SdLZbN6JqCiZnZthejq8h VoCg== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=LknwVnPl; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=I7NQYm8V; 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=349db9ee9=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) smtp.mailfrom="prvs=349db9ee9=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:content-id:user-agent:content-language :accept-language:in-reply-to:references: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=EXbAV1lYLh1Os3a0pFXylggf0POUGA4DKghVkQBsXTM=; b=gdqwclVnsOUREVuxrSMssuyLlWVQdUkUxwTUiTnX+n1oamWRjiqM1asSXyXtUK74/Q LUnfFDf9EtshN0ZpEP2Ey2BIR7EjOHiFLoo4Q+XSPhyvZzro+5Qq/DuOYfUCSSKaN8/M bj+xiZozClPVY2idvknk/80y5soLBayvs+TGWsUKi4K8N1l0dItaRdHu8htnylcnvyuO ISts3410B1QLSBYEKYlc7L5rZPORANCDP2EuSV/XmdMzI4epEsWlgpxf0HnKe19pWZrZ eQ8TMkxlz6at8ZOcNJVm+l6b3Cyp+GTAtgHNdsy+UwBXKtFT1Gs/cLfMBOa5JUiFglkZ tijg== 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:content-id:user-agent:content-language :accept-language:in-reply-to:references: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=EXbAV1lYLh1Os3a0pFXylggf0POUGA4DKghVkQBsXTM=; b=I+DFJ3HbR7AP9CE1BE497CO1YMae6mfFMnTcKFL55sa8LhwnjuvamsLieml3/vsZ2R 2LP3W7LzCOPmJjmPjKOjAzLyMxG5nHQ/4QpWwlkNu69nWuXkNzhNfqn0qZ3D6wHXDmOE Xe/rhoVBtV5HjiQTyeZG39Bs00S4XXAb//n3KZIXCYfatS33xSznjnRICDgtN8UmoViv d2yNZjYOQWs+9zqHvfZFTvK/YCsPXSz2hrFp6czHP2LKj04LBxsmuWjiVlklrYTjuYTj FoR003qhP8AFfeE5VkYaXhrS6j+MXIWYKctZsVXX9y//YWAoxJg5Z6XaAuVAskyJZjH3 Kspg== X-Gm-Message-State: AFqh2krsT6BjY8uPgpoCAPrZD3+4sdqhMvP0n232PImNc2t7yoG7oq29 Kw4LHHOxDlTWiHofsUtByhQ= X-Google-Smtp-Source: AMrXdXvZ82xhe5FzEErjHVB+gw2EGyJvx3JLV1C/1TRKu0qd00htcdys9K57aoY+ifu+wJu2+YW6DA== X-Received: by 2002:a05:6808:93:b0:35a:921f:20d3 with SMTP id s19-20020a056808009300b0035a921f20d3mr452842oic.128.1671835922070; Fri, 23 Dec 2022 14:52:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:54b:b0:35b:dfea:7af0 with SMTP id i11-20020a056808054b00b0035bdfea7af0ls1641670oig.7.-pod-prod-gmail; Fri, 23 Dec 2022 14:52:00 -0800 (PST) X-Received: by 2002:a05:6808:2b08:b0:363:1449:1614 with SMTP id fe8-20020a0568082b0800b0036314491614mr3848690oib.2.1671835920655; Fri, 23 Dec 2022 14:52:00 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1671835920; cv=pass; d=google.com; s=arc-20160816; b=e6kdVfDgdsMEe2YLeXP8gATjSd+Lm9Pi8jVnzjQe42tnUpsj13jRsYVuwlzYXk4pFP XvBAEIgs1uqwufA0TV4d2pvVzk/DbMuSjEco5dC0aoXOvd0WRgwe+S0cmXM+5LFZeP7U fsA5R74lwF7+IUjCfACadU0E7Q0Di0IgBseMak3libtSXw7jsGtUrRYcgUfCDoS0vYr8 Nzco8D/vX9INzljjSrP5PRBgoB14xQi/16GlSjxzNCLpItFdXuoQej/dDOIKwzAm9a36 jt0P6/a6apjpcbaqAlTFrijXqeIG2+QJ8bkZMMpC0ED94XA20u7vsEB1LRVo1SYotoOI bwHg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from:dkim-signature :ironport-hdrordr:ironport-data:ironport-phdr:ironport-sdr :dkim-signature; bh=DOdfQeette4v/3lbhKTJ3mHN1OQDeFHLvCbJ/fLWk3w=; b=DDE/oZost6bmIY0H5Do3KsB9GYaY70N781Qsvd8y7R9XyKpfMwe3SpDpeuAdB2phEH aqBDm7Kx4cvqTOC/VAGS+iXjml3RTR8N/zRvLtvPtF8HxxTfKJJe6Iuny5XCcBsl5aeT YcNQyJEq7NvE/loe6/MT31U3DsBklDyZoqJtV8vUzRl+Bxw3NFgNwwQ7XUuijJWTBqAA WTy22AH/c+YHpvh105NhuFTVaeGIajkLZLHCECbxXc+IDjwliOXlYPeG2z2rOeu6C0Cj oivhtJHeBsdL8/HedClxbqfILaY2kb8eOv2OzAu+EJFyiFMZm2c1ER2Mb4hJPQ/bc/T4 CfJA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=LknwVnPl; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=I7NQYm8V; 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=349db9ee9=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) smtp.mailfrom="prvs=349db9ee9=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 g84-20020acab657000000b00353e4e7f335si719025oif.4.2022.12.23.14.52.00 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 23 Dec 2022 14:52:00 -0800 (PST) Received-SPF: pass (google.com: domain of prvs=349db9ee9=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) client-ip=128.220.39.160; IronPort-SDR: hvUw33fmj5hXtUC3uQuIds1BB1KloeCLNS80CFZKTxVS6s4YpvfzgpGxIsEK3tHZJQM8OngO/S HSXm0ngBAbj5031z24ekPBM3wskYptqscvV7Rm6LM8PJJUak2qy1IrLNyT9rjA/0D3KbJkYYRD HTRPd75C8JK6ijXSj27HyEL9Xrh5et9VF2Z5rmRtqXbMmN6LRWb7Efr1Wnb9mHx1z0zscaTN7y Nqk/75wavz0c9/tz7vaw5GW0G9X2vDo+V/AWbUwc1U0HPkMg8peJbwRLvCqO9O3rUYYMu1JIuT q0wsbRJJLPQtKjwShm9gbVNm X-IPAS-Result: =?us-ascii?q?A2GRAQDRL6Zj/3uErQpQChwBAQEBAQEHAQESAQEEBAEBQ?= =?us-ascii?q?IE+BAEBCwGCLBkBawKBWIRIB5EfA4Qrl2KBQIERAwQUFh8JBgYDAQEBAQEBA?= =?us-ascii?q?QEBCAEuDwcEAQEDAQOEfgIWhHomNwYOAQIEAQEBAQMCAwEBAQEBAQMBAQEFA?= =?us-ascii?q?QEBAQEBBgMBAQECgSYNVw1dC4FEC4F0CwMxAQyCOAUCAwIkC2RNAwMzAgEBA?= =?us-ascii?q?QEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQEBAQUCDQdKAQciTwEBA?= =?us-ascii?q?QMjEQwBAQwsDwIBCBgCAiMDAgICLwEUARACBA0CBAEBAQEZBIJdAYJuAzETs?= =?us-ascii?q?H4FTHqBMoEBgggBAQYEBIE4AZsSGEYBCQ2BXgkJATJYLAGDR4VHiBRDgUlEg?= =?us-ascii?q?TwMgkUCMD6BQoEgAgKBJAQBAQcLASEXg0CCZ1c3gSsDKEooA4EDKwKGShqBH?= =?us-ascii?q?xkCAoF/gj4BBIFMHQICAgKFS4E9fYEpDkccJQQOAxkrHUACAQttCkABNQkCD?= =?us-ascii?q?EwrEwcbB4EKKigVAwQEAwIGEwMiAg0oMRQEKRMNKSZrCQIDImEFAwMEKC0JQ?= =?us-ascii?q?AcVESQ8B1Y3AQQDAg8fNwYDCQMCH1JaFgIuERUFAwsVKkcECDYFBhw2EgIIE?= =?us-ascii?q?RIPBiZDDkIhFjYTBnoNCw4TA1A4gRYEL4FoBlGadoIbgT+BNBESEhwtNhKSR?= =?us-ascii?q?oNGmFCSShmBDg8xg0eLU5R4BkGFSqNal0YgilFmgW+aDwIEAgQFAhaBeDQsM?= =?us-ascii?q?HByE4MiCUYBAgEBAQ0BAgEBAwECAQEBCQEBAQGOHTeDO4JkgjCFSnUCAQ4qA?= =?us-ascii?q?gcBCgEBAwmKJIF/AQE?= IronPort-PHdr: A9a23:HRUSqx1nRNDLwr0/smDOGAIyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaCo6g2xweQFazgqNt6yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6y9pHJYwhFijWxba9vI B6rsQjfq84ajJdtJao21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2U bJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5 KhsVRHolTwHNyYn/27Llsx+gqVboBe7qBx+xY7ffYWZOfV6c6/Ye94RWGhPUdtLVyFZAo2yc ZYBD/YPM+hboYnypVUBogexCwajH+7v1iRHi2Xq0aEm3eksEwfL1xEgEdIUt3TUqc34OqgVX +62yqfHzyjIYe9V1zny6obGdA0qrPaSUrJqcMre10kvFwfeg1WSqYzlIimZ2foQvGiG9udtU /+khGE7pQ9ruDev2tsshZfThoIT0l3J9yp0zYk6KNC4VUJ2bt+pHZRTui2GKYZ4QswvTm52t SsnxbMIt562cSYFxZop2hLTdvKJfYaG7BzjSeufLyp1iXR4c7yxgBay9FKvyuz6VsSs31ZKr zZFktnRtn8WzRDc9s+HSv5l8keu2DaPywDT6vxfLkwulKrbLIYtzaQqlpscsETDADX6mELsj K+Zbkkk/fWo6/jjYrXhoZ+cNJV4hR35MqQrgsC/DuM4Mg8BX2if5+uwzqHs/Ur8QLhMk/Y4k bHZvYjHKcgHvKK1Hg1Y34g55xqiATqqzs4UkWQZIF9LYB6LkYnkN03ALf39EPuzn0+jnTZuy v3FO7DsAIjCI33Gnbrge7t29lRSxxApzd9F4pJZErQBIPXuVUDvrNHYFRo5MxCsw+bgFdV9y psSWWKRDa+dN6PfqVCG6P8uLeeLeoEauDnzJPk46/PvlHM1h1EQcbOn3JsWbnC0BO5pLFiDb XrugtcBDH0GsRQjQ+z3kFGCUDhTaGiuX68k+z03FJiqAZrBS42jmrCNwSm2EoNMamxbFFyBH 2/kd4CeVPcNbCKSLNVhkjsBVbW5VYAhzxCuuxH6y7pjNefU+C0YtY/52Ndr+uLTiAk+9TpvA MuFyWGCU3l0nn8URz8xxK1zvFRxyk2f3qhgn/xYCdtT6utLXAc9MJ7cyPB6C9fqWgPBYNmIS E6mTcu4DzExUN0xxMUOYkZmFtWtiRDD2CWqA7sLmLyEHpw09b/c32DqJ8pn13nG06wh3BEbR NBSPzimmrJn7FqUQIHTlFiBjOClcqMT2COL/2CGimbJuVpXUQI3caLAWmwYflrqvMz02kPPS KW/Tp8OHRJfkOmuN4sResHyo0RoafrgOsv4Qz6KpkH9XzyE++OmNZbnIVc57GiHIm42iDk38 F2GJQdzWn+kqmPaSjNrHFPrJUjr9LpDrmimRHM53x3fb1F9z6HnvVkan/uBU+hV0bUDtyMs7 T5zGRGxmNfNBNuM4CpmeaJAZsss3EZf2F7ZugtnL9uLBo97mAc5XxlX5FPyzDtmJKhNkso1i lN29zdUZPiy3G4RXWqE0MrCHo2acEPUzguWT6P92kHRnYrO/64O7LI3rlziuEeiEU9xz3Iym flS1nyA4Y3bMBsKXK7xX0Et5jB1oLbVZiQy/YTJzWYqOq6x+HeW+9UsA/ci0gecbs9SDKOJE xXjO8IdAMeqJeMwnEWxdVQPO+UEp4AuOMbzWt6n/J/jBsdNvBbu2Wld4Y191mqO9zc6R+LVi cVWi8qE1xeKAm+vxGyqtdr6zNwVDdlaNma8yC2xAolXa+UyeIsQEm6hLoWxwck2nJ/iXXNUt TvBT1ML0cOkY1yeOlr62wAD2UEeu3fynyy+wnR9mC0oqazK2ivIzqzieRMLN3QNSnNliALuI ZXygtwHDyCV IronPort-Data: A9a23:0BDFOqkng4V7NPaQdervIbbo5gxnJkRdPkR7XQ2eYbSJt1+Wr1Gzt xJLUWyEMquPZGHwLYh2O4W0/U8D75TcmIJkGlRorC48QS4T+ZvOCP2ndUqhZCn6wu8v7q5Ex 55HNoSfdpBcolv0/ErF3m3J8CEUOZllwtMQMcacUsxLbVYMpBwJ1FQyxYbVvqYy2YLjWlnX4 oupyyHiEAbNNwBcYzJ8B52r9UsHUMTa4Fv0aXRkPZinFHeH/5UkJMp3yZOZdhMUcaENdgKOf Nsv+Znilo/v10x0Vo76yOaTnnoiGdY+NSDW4pZftjPLbhJq/kTe2Y5jXBYQhNs+Z5xkULmdx f0U3aFcRzvFMYWWpNQyXDxzExhvIKB/+eDuEUmbiMmqmhiun3vEm52CDWkbBqI9xtlaMTgQs KZDbi8MaFaKi6S0wK/9R+Vx7ighBJCzetpA4Tc5lmufVKx9KXzAa/yiCdtw0S0xi8BKNfTee owUZScHgBHoP0MTZAxPVshv9AuurkTYdzh0lUnJnrMUxjXN7jdVj/+9C9WAL7RmQu0QxC50v Fnu32P8BQ0dLM2j2CKIznKhgfXetSz8X40WGbKi8eNymxuYwWl7NfENfVagrvyllUOuAowac RdS5Sso66E+sk6rU5/wUwDQTGO4gyPwkuF4S4USgDxhAIKNi+pALmRbHDNHdvI8s8o6GW4j2 lOTwIHrBSEpvbGIECrP+rCRpDK0GC4UMW5bO3FVF1desoCyrdFhlA/LQ/ZiDLWx0o//Fwb2k mKDoyUJjrkOidIGiveg9lfdjjPy+pXEF1Zn5gjeUm+/wBl+YYqpO96h5VTBsqRCLJvfQ1Wc5 SBWl8+b5eEILJeMiC3UHrtcRu3ytq/UPWSF01B1HpQn+zC8wFKZfNhdsGNkOUNkEscYYju1M kXdjgUAtpZcMUyjYbJzf4/sWd8hyrLtFIq5W/3ZMohOb5x2eFPV9S1ifxTAjU3Wv20QrowPY MneK53qEnccT61riji2WqEQ3aJynnIywmbaRJbayRW70OPAOi/PFexUaQqDPrIj8aeJgATJ6 NIDZcGE/BMOAuTxbx7e/ZMXMV1Xf2MwAor7qpILe+PfcBBqHnotV63Yzb87Idw3sp96s9v30 0HkBAoCkxzghHuBIAnMaHB+Lr7jQM8n/348OCUtO3eu2mQiONjxvf1DLMpuLLR3pvZ+yfNUT uUef5nSCPp4TGWV8jsQWpDxsYh+eUn5ngmJJSekPmQycpMIq9YlITM4ktYDLBUzMxc= IronPort-HdrOrdr: A9a23:Xih6s6MUZaBJG8BcT07155DYdb4zR+YMi2TDiHofdfUFSKClfp 6V8cjzjSWE8Ar5K0tQ4uxoWZPwCk80kKQa3WB/B8bFYOCLghrKEGgA1/qp/9SDIVyGygc178 4JGMIeaOEYZWIKyfoSizPIdurIteP3l5xA8t2uq0uFIzsaCZ1I3kNcMEK2A0d2TA5JCd4SD5 yH/PdKoDKmZDA+ctm7LmNtZZmPm/T70LbdJTIWDR8u7weDyRmy7qThLhSe1hACFxtS3LYZ93 TfmQCR3NTujxj78G6S64bg1eUWpDLT8KoCOCVKsLlXFtzYsHfnWG2mYczBgNl6mpDr1L9gqq i3n/5pBbUP15qWRBDznfKl4Xie7N4jhkWStWOwkD/tp9f0Syk9DNcEjYVFcgHB405lp91k1r lXtljpwaa/ICmw6BgV3eK4IC1Chw6xuz4vgOQTh3tQXc8Xb6JQt5UW+AdQHI0bFCz35Yg7GK 02ZfusrMp+YBefdTTUr2NvyNujUjA6GQqHWFELvoiQ3yJNlH50wkMEzIgUn2sG9pg6V55Yjt 60e5hAhfVLVIsbfKh9DOAOTY++DXHMWwvFNCaILVHuBMg8SgfwQ9Kd2sRH2AhrQu178HIfou WwbLoDjx9NR6vHM7z+4KF2 X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.96,269,1665460800"; d="scan'208";a="464630629" X-Amp-Result: SKIPPED(no attachment in message) X-Amp-File-Uploaded: False X-MessageIPDirection: Outgoing Received: from esgmtwex16-23.win.ad.jhu.edu ([10.173.132.123]) by IronMTW6.johnshopkins.edu with ESMTP/TLS/AES256-GCM-SHA384; 23 Dec 2022 17:51:59 -0500 Received: from ESGMTWEX16-21.win.ad.jhu.edu (10.173.132.121) 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.16; Fri, 23 Dec 2022 17:51:58 -0500 Received: from NAM10-BN7-obe.outbound.protection.outlook.com (128.220.36.248) by ESGMTWEX16-21.win.ad.jhu.edu (10.173.132.121) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2507.16 via Frontend Transport; Fri, 23 Dec 2022 17:51:58 -0500 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=A4Kr6X2C9PqIUaJAM3WeRD30ENJ7BlG0kthpGoFQa6CJv+EXHeNk69Zuj60SrVeuYzesXw9dmwQdbATlQs0fv7ozcZ09XH5AXhe4zJB7cMcLvbveNluI1nyVP+yy7qalLD24AVb2paTLJe7Go0OVMc4iWz3G8yyPOI0W0MKX3SSOHNX7AKQkxPtVSaQ0Q7B49pHSM9Xt9RfFIbL7NbQ0PT/whnTw92OlL4H7GHFU2guo3mWEZpm8NB5y47dX28WLMaGLZYGFfd6aSJd+Jc30qpU3Ck6iPgH0CM1JcBNwCD8FVlMwUnpCowkPqUWepQMMAbg2RV7ooZghX2/YuneArQ== 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=DOdfQeette4v/3lbhKTJ3mHN1OQDeFHLvCbJ/fLWk3w=; b=nUSnpQtz23Mn3BX2w8tuev+VEILiIZe9fxi/fTBbwhOlkLUAYcNxsRz1e2XMh61RkLWQntpPAIshy3OIuJaf4lOlGUD7KS+rIfAsbALhaGCS2w645ZQ0aWZ+ximkn10XQqweCsNTlePlYStNRTCcbPPAYOJ1rf/rH9QsHS6h73mFrSG16jwgRMBmQnKtBWLrqrydgloZPBqhTdK+/gqno7dEREGZgjlFw0Yjlx47WV/CCXf6tfI1k/QFHG2/5dpfrjKluuWBngoCVu0FKc2qJoLNPzboHa3HfgXkaHk0C4MSuZyEx8O1pgvZvSM0yvpy4XjaZJUu76kdLXQvVfhs9A== 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 DM8PR01MB6984.prod.exchangelabs.com (2603:10b6:8:19::21) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5924.15; Fri, 23 Dec 2022 22:51:57 +0000 Received: from DS7PR01MB7758.prod.exchangelabs.com ([fe80::3647:6adc:90e:97c8]) by DS7PR01MB7758.prod.exchangelabs.com ([fe80::3647:6adc:90e:97c8%9]) with mapi id 15.20.5924.016; Fri, 23 Dec 2022 22:51:57 +0000 From: "'EMILY RIEHL' via Homotopy Type Theory" To: "HomotopyTypeTheory@googlegroups.com" Subject: Re: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv Thread-Topic: [HoTT] My Introduction to Homotopy Type Theory textbook is finished and on the ArXiv Thread-Index: AQHZFrSWe86CFFROhkuQsQwTLMZ8Bq58FTuA Date: Fri, 23 Dec 2022 22:51:57 +0000 Message-ID: <7e2fee3c-30e8-a3ec-8941-68c63538240b@jh.edu> References: In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101 Thunderbird/102.4.2 x-ms-publictraffictype: Email x-ms-traffictypediagnostic: DS7PR01MB7758:EE_|DM8PR01MB6984:EE_ x-ms-office365-filtering-correlation-id: ecb7ecdc-55ee-4f7d-c8f4-08dae5384b5a x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: C7He+vyMpfx2yZl/eqaU/VCy2psaw7Au4W3ChAX66I6yXdoToSf+qegcFROas05CUG0mlhnMGqUQIUmiVq7+XxBB0H4R+ebh6Og7yujw/1KT3k+yhuha1Jb8zgF3J2nZhYoEi4RNsU+giPdl91hKTe8OCB2bNTYWWmMxVcNLQ0ETGe/9LpqiJYLtS9kqNlKirLMe/CDcAP179GyjCFyc1HXA+fY0dbfBrDvBy/Rc9Ds0wJrKjzKDl1o7s0uGcMGu5z+DhlxVtWyquDrWcOnsCyTRvSsYBlMl+qpj8ffjZ70pU9thSuvC+GGKHJM4chVH/64AuqMl+eMLJSjZiIugYvt4cLBhuaEsFOtGQG3FzzJYy4Ojbq/4hd+geFsHjnfp0a5wFRbpg8ycCORjMfKrEQSfhBMp93IUFYy894RaCiK4bgRrpRQb/WpQAJnxOclHI08Jj3+VVq9Sx6QIgXrmwW0/O5tob+8aObq9qK9Cdo76VC5NhGjJByUshmrIShdIMpyU8hFBvZoMLVINRZUs1MufVLhezo3y/+aU1tbPSLV8ZBGlY99Xpgq07dJ6IQ/GOvHm675GcuEZ9nA8EzHdIszHH/2abceFmU1S3I9PM1ubRRbUpvOsGYjS8/WASZi8mPZRxarxpuan01uyVXCgDGvnr2j+G69Fo+8hMuLuj7I0lN98dv5bjfmfVcN2TmHZC0hoZrISQU6UjE0+tFy+PdoMVJXz04IhvRaZICUi4qcHx7Sz01C0fyWicP6fSRIdy2pUdwdFQT1hgh88c4LPJ+xSVMeFCr1Sm546XrNuaAU= 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:(13230022)(6029001)(4636009)(39860400002)(376002)(366004)(136003)(396003)(346002)(451199015)(66899015)(31686004)(9686003)(186003)(6512007)(6506007)(91956017)(6486002)(26005)(64756008)(76116006)(66476007)(66946007)(66446008)(8676002)(41300700001)(5660300002)(8936002)(66574015)(83380400001)(966005)(2906002)(478600001)(6916009)(36756003)(38100700002)(122000001)(53546011)(86362001)(786003)(41320700001)(31696002)(66556008)(71200400001)(75432002)(316002)(38070700005)(43740500002);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?dHRBaGZ4UXZSbUVIUjhhdEg4ZCtxaEdVZmpWWGl2NmluckY2ZDFvczEwNnlJ?= =?utf-8?B?TW9IQ2tDamJ1WjY4T2tMbnFWTlh0ZmljUTlqMkc1VkUrakJXNTZEQTlGa2Zz?= =?utf-8?B?U2VvM09xdUlaYy9yaGRmOUZ2Q2YvOFlsSWVUN25oeXNxNStBQ0xiL2hhUVU1?= =?utf-8?B?c3JtcVBieFZjRGMwOHlkU05QSjlJSldXUXBleGJndzcwdVRtL2ZxZzFDZ21r?= =?utf-8?B?OE4xS0oxblQ0OElpVm1QMytDcmNYL016b3ExQWJVWFBlNCt6VDNhUTkrSUQr?= =?utf-8?B?RklWU3FVNGZseWlhQ0NLN25QR2VnODJ3Ukp2TUxuOGFIb1ZEejNyWEhRTDBG?= =?utf-8?B?YUNSQzliQjFUQkw4T2N5ZGZQZFhpZWcrWHUxTnc5Zlc5NE1ncFVPSnQvNDVw?= =?utf-8?B?Mmw3S0d2aXI1RlY1eFQ2d0FRdFcrakorTTV1TTZDbHMyckQvSUVDTjR3YUhU?= =?utf-8?B?U1dqVkE1dUx0OWpuVmh2VU5yWDRmb0twUU5kMUFwUitNWnhQT253dnZjOWxk?= =?utf-8?B?aDNNY2JrZmR3aFVjSkJGOEMvVXJhVW5NdGk3M0pFVEwyY0lFMHVKMUVkYlZU?= =?utf-8?B?SFA5dXZ5RlRIbjhMSGtkODd2U0hoOGlEQllJdTNPQ3A4eDZYRUJXOUkwc2Va?= =?utf-8?B?UXRnTDR6aCtoNUVuenRkaW5pSmFqZk1mNkFrdm1SOExpMXZaWUt4bUdoWnR0?= =?utf-8?B?SDI4WitvMTRhcFFISS9YL2xaVUcwYk5saWlOc3F5dlB0b3BLM0cyalNHdUw3?= =?utf-8?B?b2NPelU4ZEVmYVloNmtnVkNnOVNUM3VHVXI5NnN0c1F0TXNiWHpMTCs0WWhV?= =?utf-8?B?cUMzdWR0RmRoVHJTbEZSblRiZ1N1QlZtdjNsRmdzbXNrc2U5T0RLVVJ0Z0Z2?= =?utf-8?B?L09qMXRCaGw1Wk5ZV0U2YnFWbzRzSnNTb3JSU3U2SVlnWS82czBqYm1sL2k1?= =?utf-8?B?WUVLQTdlYjF5aDBzNTFQdHE0amVEZXdIaXk4QkVsbEMwVTdtRlBSZDNZTXZq?= =?utf-8?B?OVFGNW5MUzNNZU1Qa2RwNHh1RmVRYnc4QWFQS0V0UC9ROW9tOWM1V3d4S2xD?= =?utf-8?B?dG1hbnRZRTZsK0x2UGpmaTFFZ2R3aEluT3IreW81K2ZMVUF3bDNYQWoxMm52?= =?utf-8?B?d0JObzYzK0Q3blZRN3F0aHNzeGZSbU5ZSGUrcWdtMjFjMnNWc2FFMlR1ZHo1?= =?utf-8?B?UHcvc3ptYzhVMGZnRVFWYXBlandPSEVJQzBGdHIxa2x4T3RUc1lUalRwY3NH?= =?utf-8?B?Y3kzZkJ3cThBTnlZVExnaWxGeW9raEk0emx5aWRNV1VmTHBFY3pJcUJNVmkw?= =?utf-8?B?SW1DRkdHNFRxOEMwdW90Mzg3NE9ENEtuQyt0aE5VaEZ2M0RPZUNxM0p3djFx?= =?utf-8?B?a1g4MEhCZUJMT0dWUDUvN2N6OER3Tm9MVGFNaFlDN1lTc2xKd200K0J5MEkv?= =?utf-8?B?K1NWbFphRzFZSUU0RFZKNnl6WXk5RlRSclNBeW1ZVkwzTWhLZFgwY0xhL3ha?= =?utf-8?B?bmNJbmZtR3o5amJRRnhqUzBTUFB1ajhtd3VhMFhIK2ZQMG53MXhlMGxENy93?= =?utf-8?B?cjBoMWxWaEFBYXhuU2lHN3RCZGdQZmoyK1ZXN1hqRnFMMnFaRmFWSGdzUklS?= =?utf-8?B?dmM5RFFEWitiUkh5OURqbTB2dEtVR3QrcFFjck0xOEZkQWMxaGNhR0h1bC9M?= =?utf-8?B?elU2MUl5SmJTNXVxUkwxZ05WS0RUWE9sL09TaVlGWmw0b08yYXRxTTEzK1Iv?= =?utf-8?B?SnQwU1g0d1ZzL0JQM3BLdjdNMHYxelJtaU9xM2ZlNGIySDBKVjNjNVpvNWJX?= =?utf-8?B?VFN5NjRNOFp4anBLNVBZTURpU0twQXBVeldHYk9RUSs5dURWKzB1d2pMWis1?= =?utf-8?B?Z2g0K2VNdkNKQ1B6WWxBNjNyRnF2d0hNM01KTnozSkNaMWk3U21WdmFzNFBy?= =?utf-8?B?V0phNEdlRzVEM2crWnlCeGlZNzBwTncydTJkSlNJMjRnVGN1Q09kT0R5OEto?= =?utf-8?B?VVJYbTdRM05kOEsxcUszemNXUVZ5Q0xTSVNzK01IbENSRzlZNkxuUnQ1MDZC?= =?utf-8?B?MzhwK0JCanF3MURiWTVSVFd5NWpIb05SeXJqWVhHYXBZcGhQKys1V2IweTVW?= =?utf-8?Q?cHFf3fUNT7DmAJjH99eQkbiOc?= Content-Type: text/plain; charset="UTF-8" Content-ID: <914537C78FC3D64D9442150A00521148@prod.exchangelabs.com> 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: ecb7ecdc-55ee-4f7d-c8f4-08dae5384b5a X-MS-Exchange-CrossTenant-originalarrivaltime: 23 Dec 2022 22:51:57.0891 (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: fMukayTlOM9MWdrTqxECohsVVVGw/OKfXS1Ji+zXTopId+BgdhrnlNCh2ZMpu3Y5 X-MS-Exchange-Transport-CrossTenantHeadersStamped: DM8PR01MB6984 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=LknwVnPl; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector2-livejohnshopkins-onmicrosoft-com header.b=I7NQYm8V; 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=349db9ee9=eriehl@jhu.edu designates 128.220.39.160 as permitted sender) smtp.mailfrom="prvs=349db9ee9=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: , Congratulations Egbert! Last fall I taught a topics course on homotopy type theory following this b= ook to an audience of mostly mathematics students. The weekly problem sets = were all in Agda, drawing inspiration from Egbert's excellent lists of exer= cises and extensive formalized library. Course materials are available here= : https://github.com/emilyriehl/721 I mention all of this to say that I had an excellent experience teaching us= ing Egbert's book. I had to skip several topics due to time constraints but= I never found myself wishing the material were presented in a different or= der, which is quite remarkable. Kudos Egbert! Emily Professor of Mathematics (she/her) Johns Hopkins University emilyriehl.github.io On 12/23/22 04:54, Egbert Rijke wrote: > Dear homotopy type theorists, >=20 > My textbook Introduction to Homotopy Type Theory is finished and availabl= e on the ArXiv: >=20 > https://arxiv.org/abs/2212.11082 >=20 > From the abstract: > This is an introductory textbook to univalent mathematics and homotopy ty= pe theory, a mathematical foundation that takes advantage of the structural= nature of mathematical definitions and constructions. It is common in math= ematical practice to consider equivalent objects to be the same, for exampl= e, to identify isomorphic groups. In set theory it is not possible to make = this common practice formal. For example, there are as many distinct trivia= l groups in set theory as there are distinct singleton sets. Type theory, o= n the other hand, takes a more structural approach to the foundations of ma= thematics that accommodates the univalence axiom. This, however, requires u= s to rethink what it means for two objects to be equal. This textbook intro= duces the reader to Martin-L=C3=B6f's dependent type theory, to the central= concepts of univalent mathematics, and shows the reader how to do mathemat= ics from a univalent point of view. Over 200 exercises are included to trai= n the reader in type > theoretic reasoning. The book is entirely self-contained, and in particul= ar no prior familiarity with type theory or homotopy theory is assumed. >=20 > Over Christmas I will write a blog post in which I will go more into the = content of the book. For now: Enjoy! >=20 > Happy holidays to everyone! > Egbert >=20 > --=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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com . > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/CAGqv1ODuH3xtsFyFEekjwNH4SUN%2BdU8B1te2ZLX%2BNZsQLeChx= g%40mail.gmail.com . --=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/7e2fee3c-30e8-a3ec-8941-68c63538240b%40jh.edu.