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 16014 invoked from network); 8 Mar 2021 15:10:53 -0000 Received: from mail-pj1-x1037.google.com (2607:f8b0:4864:20::1037) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 15:10:53 -0000 Received: by mail-pj1-x1037.google.com with SMTP id y5sf7452896pju.5 for ; Mon, 08 Mar 2021 07:10:53 -0800 (PST) ARC-Seal: i=3; a=rsa-sha256; t=1615216249; cv=pass; d=google.com; s=arc-20160816; b=sPKN/cMSBqJI6M2fRxQMRKmtB+EOQTiO1NDLC1wVPncIrbtX2wwd/sDmHVe/FZHMUb catQN7eXE+5GnXPhYk+wKIn3mhxt7LASjzlYC7Mujm7XJF1pgaQDLZw4VsiXxqZwSzhc SIVs/cQejkta+oyUu/jMV0V7SDibNLtwj/X5y0zr88kP1QKDN3TAxxIHKDTQ4+K6/29a 6XHP7aOaZ47JucluV9oli0c+c/HF96WVXGX9/5cngxcp4PdYgHbGngarzyfI1BUIUAiD uVIuNBiiqH0aD8obAEW/Xz3Lkcuz3kJdodL7FIE/PpOuLm83+4L0R+QT2qfrLqQE1tKl A3/g== ARC-Message-Signature: i=3; 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: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:sender:dkim-signature; bh=6qeM3A9oQhnaEwYNnXn75ALRmFoVqqJR8d1UhVcEXkY=; b=ED3VQnw4SvcfZSyRe7r6cH9jvkrvH4mUWM2mppA5mYHUF8GOSeK/xzTomMUD8NStoj SxDRh7RVwRc6VbWKcYjS0OyL4mJKv6PBZ5lLLrPj6Y2Gv1Ch5yI82W+jZQ/TgxqUKDNG ls43aM3wbTcSII0m/XD5SRCbby9Wm7nhTriOSYx0tSJs3Fp42jGSY+wNoKcot+Z3a+QA 9Z3ToPxFpOicdgCSys84Y3mAN1IfR0zeHGMJSn5DETbP1EhY3QluEo/mMSmlf4U6MLTk pfXqsYma4/KnFMmVPa5eI4eY23yyAS5mHTQuzBb8hCA4ONkhsV2+HIsX7MA5E00yBM7m QhKg== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=oTagIX42; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.66.93 as permitted sender) smtp.mailfrom=jdc@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :content-id:content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=6qeM3A9oQhnaEwYNnXn75ALRmFoVqqJR8d1UhVcEXkY=; b=hcV644TZ/J/+lGDrI8dg3QAfFtwgEfnOo7BTnlxZfRGKHMbkmhuxasD8e3YLNFAuoJ DIYEfbU6k1gIt0yIF53DaalSVBG1V+TMDnBuSmDQ6mNzZrcPz+F1cYjs8jcoQrFdFz0V yUjTZRUb8Zv8gvZ2uCzoYDWSWwwSGXt7U3gyuv1y/NHlJX0cStg0wXc+7i9mL1OiyVOF xJKDb4q7NppLPD4C4MSofqtTqa593PLpIB0P2jTr0uPlRnE63evGM1MLETvb668hq5Tz g8s2QdUy8HGYU7zdcG0BywWDDQBu05Uc0zCfI1fE6gNIRuN/+zS7uN5xvtAXgyAOPoBC tRIg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:user-agent:content-id:content-transfer-encoding :mime-version: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=6qeM3A9oQhnaEwYNnXn75ALRmFoVqqJR8d1UhVcEXkY=; b=iFLrMY5GBNn/zF7/V36Hb0vROy1iHNuOzJ8OLZzgjYSitZWdKdptUCwtsch4i7VzRh qAwgKPHXZ83Zj2dWkD4V9eBN1rboPHy0VDc+2CiqrS5JAHzw4nQu0Wb/+iXKGbhYoBNg IarkiZ4t/A9h1/5EvMbIIan118/71mXQE9gV+XEI+ZtvV1dZ1Q0kxoDIWouEI4LrrwlJ SFLquoqqkDHahcr0ksWBjpCtycK24ZSsCXG6vOBHUNdDuJwlzdk2+9rEcBy8ixpr77Yy gbjHO3nZyw9CQOcrV7rbCqR8UEKAaNAkjtrL4FsiUOZWf3lpZLm6z/76+MlQXeYKWvo2 vmow== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530WFV8QEWa8NUHCB0OLtz48ejw+ET5UXqKVf0hY6kzS0rtO3yCC lStBMQaK7PlpCvPZNYg2dXM= X-Google-Smtp-Source: ABdhPJxR+/hMvYNJUUKQiac79dqjkWoszohdzqNNgXg2uqYZTNURFEWd2g7rF4FDr1r4cO0XTgupfA== X-Received: by 2002:a05:6a00:238c:b029:1f1:5514:cfd0 with SMTP id f12-20020a056a00238cb02901f15514cfd0mr15840255pfc.36.1615216248826; Mon, 08 Mar 2021 07:10:48 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:1914:: with SMTP id z20ls3445738pgl.0.gmail; Mon, 08 Mar 2021 07:10:48 -0800 (PST) X-Received: by 2002:a05:6a00:15c8:b029:1b7:d521:32e9 with SMTP id o8-20020a056a0015c8b02901b7d52132e9mr21408582pfu.22.1615216247887; Mon, 08 Mar 2021 07:10:47 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615216247; cv=pass; d=google.com; s=arc-20160816; b=XV+Mj1maFb3gHrQ+ASf0VjZmaUfiPvzTNUjTRiimOoAWVrEQL/Tyju05BKJCICbt7L cLpvCOPVfYOJ0upnMx8yP+3n9FoNigsPKJs+9CoZJ98QYHQ64q3JwG+bmLZcy39y6rbM vemCG6OXdqgh6kH3c1dGYgWQgPoqDEvhL6yUA8f3ngTuPaUKJsB4YLB6335fKFQBnIF3 vgkOMIyG4DEGdMciPSFCexiHmTBZz2yrEWSoo+0OFy1k3I1fMdVF8QavL+e6yeO3p4dS z+D8Zw5nQLe50teYG30gcvzW82i3L7iGJcEOnm9I1VtpOMUSYihY8KXyQV5LwClM2zId GCMA== 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; bh=+3TXNcBs3Z4CR8VySNOHlRGFXEyK6M3QlGihKjXS3lE=; b=fhw/5LsryYtdBMPDs9mKqN/0bXoPzgunQurbvPf4k1mTVg6fww86RTg91LVSTrHfj/ 3SF/3/AoCvN/6Xx+0sXHK7ILSwTibqkeaughSUHY2cu1S9RTlAp3vLgIR5EbtfOD0pDj P+wMUmSoVTwKh5bRsdoFAzdMyQ1v/1tlht0QrLh7H42OeACRUoQFNurkmlp8VJgNPRgC nuLaoQv2e0nzpSAww6gnRYOrm9UrlMBwW7A+eq+YGnUTb/79KzMIp24YE2B/+30AdrkB DVPIxK/h9P4pmkaqG0ketsHXv9DXRLVzeRSbMYsYbxCUPkGQK+vuy0pp/47dCBgGy+Fm fduA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=oTagIX42; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.66.93 as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-QB1-obe.outbound.protection.outlook.com (mail-eopbgr660093.outbound.protection.outlook.com. [40.107.66.93]) by gmr-mx.google.com with ESMTPS id b3si699106plz.4.2021.03.08.07.10.47 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 08 Mar 2021 07:10:47 -0800 (PST) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 40.107.66.93 as permitted sender) client-ip=40.107.66.93; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=JxviFYTIhiDEQ3yq1FwREhIRjd8NSkxBqwSdH79XnMAn0iNrzNctr83ed58M7f4afQg2zx9vTpmM56AkROrw55cnXXAT0Ms5RFnUQBgj2lJhVjnYtYwk0foEfLiH0vp0apFw3iUCc1+UnIyhrT/ara8yh3kfUP61k+Vsy6n/WWTRqrWEdTXYSvlHRFrYUEJ7kG7hCVQGERpNewnrhSSvnIfDQ+lhpcAX45gCM8rZhkafsFzSFpSzSe8+cmgkWPNulFCn5a0+TI3gYLSPvoFNA9ET7I7ZJGg2pE9MY6OHfSjVvZ96X7rEuzuyT8iqOfvPWAVktD2OksQD4uOjK75Lgw== 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-SenderADCheck; bh=+3TXNcBs3Z4CR8VySNOHlRGFXEyK6M3QlGihKjXS3lE=; b=GLE3i4zo75LYfAxvfY03+ohrI9Q3KRoY5GKSNAo6rBQU/9Ikh97k5TLswAOpmVy3dYZmuk7CstiFj0RukWV3h6iaKFRfFEaivE3KMLfLTrW6q42GI5n7H33cCB8yz/lydKeoHU2WTg9rij3Aj0roAZtAdOlsyD4DI/e+Gw1u2SfGoEqWz/MVbEIDRAKuDfZ9T3iXxBnGcm3dvru/2xFNYkqDiMgKA330LCP3Sh5uxb7ODi2smnohloW6DI3pTEyKF6Iidzpm3Hd8x4ELQpfw12iVMZksSSmjul6FEvOxjjaA3Ma2cj1xLc6hdmS1KFW+hGjSsbaIpnQHQHiJ7kzPmg== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=uwo.ca; dmarc=pass action=none header.from=uwo.ca; dkim=pass header.d=uwo.ca; arc=none Received: from QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c00:30::22) by QB1PR01MB2402.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c00:39::22) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.3912.26; Mon, 8 Mar 2021 15:10:46 +0000 Received: from QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM ([fe80::694f:acf5:cad4:3019]) by QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM ([fe80::694f:acf5:cad4:3019%6]) with mapi id 15.20.3890.038; Mon, 8 Mar 2021 15:10:46 +0000 From: Dan Christensen To: "homotopytypetheory@googlegroups.com" Subject: Re: [HoTT] Syllepsis in HoTT Thread-Topic: [HoTT] Syllepsis in HoTT Thread-Index: AQHXFC03TdIT59TaFEqeHGDRiVK/8A== Date: Mon, 8 Mar 2021 15:10:45 +0000 Message-ID: <87blbtk7ey.fsf@uwo.ca> References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> <7d4b6fd7-3035-e0b9-c966-97dd89d8b457@gmail.com> In-Reply-To: <7d4b6fd7-3035-e0b9-c966-97dd89d8b457@gmail.com> (Kristina Sojakova's message of "Mon, 08 Mar 2021 15:31:13 +0100") Accept-Language: en-CA, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) x-originating-ip: [99.243.22.114] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: c76577b0-3810-4399-53d7-08d8e244598d x-ms-traffictypediagnostic: QB1PR01MB2402: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:7691; x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: Qqkezlz75DFPOrlHQlgnx7FxBHIw85f7r5GYtvCiCMaPdYyFx/2HOl5I/+GUA6R8y5ke8FiKrII4OOuNg+aJ3f5Dd7/hcdo4p33RuS9ZTwh1a0uGjmOFPqwrDStxtcA6DDjo7BPFfusUAwqkZqk8qt//Y4d41Pv1KVQHEd4SqFz4PbIVJstLWNzHFh0qCxfSOMafP0HiHe0YsfP+FGXBwjhYtMTzT6gVhipwpK/iDBTvkYutYC5mEAU4LjqKUwT0qS+t2XBLgMbxCpDeox9yExXOZWMxLDT1oX9BE7IOakPzdCpLlj45SGENwCFK5ZyZbfkbqPeTG3EuXZr++o/5yVcXfh4whqiQTtbpA9wq80gAaFvuTzMdl7XT8rN5kbj8itfInYL4ra5s9EvcJEVm1rg3YI5aDz/hlF42osmSRS6bDv8z1ltNE+8Zv/5c5S2yF2BEEzCiIIZ61u+VJbYDqvSs+rd9bJbVTf3HHREaXtD33uV3QG1SEzSwAYmnApUFV/rTdsdAbA9yW0W+qn5GJgmYRg0bHuo5wkytaEzwNvy56ZBcVy0XHzBbWndmZ3BUItu9wsxR8f17oH+GiU8OIw== x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM;PTR:;CAT:NONE;SFS:(4636009)(376002)(396003)(346002)(136003)(39860400002)(366004)(786003)(8676002)(2906002)(8936002)(316002)(478600001)(76116006)(6512007)(2616005)(66476007)(66446008)(66556008)(6506007)(64756008)(83380400001)(53546011)(6916009)(91956017)(5660300002)(66946007)(86362001)(966005)(26005)(186003)(36756003)(6486002)(71200400001);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: =?utf-8?B?SzFiQjAzWDdRQm1WcDF0ci95QUJQd1lTYjVNMzE4aWw3L2F0SzBaR0Y4Q3hq?= =?utf-8?B?SGtqSVVlYVN1bGFma0twcmlNdHF6TUZ1NDJ2b3ZxSWlncC9GcWoyMkJ0Skpu?= =?utf-8?B?b3pJdkxwM2IyTmdSTGZxQnJOY1l5WmRQdGNnbk5pbmx2WWZHNEllK1pVYTBL?= =?utf-8?B?VXVDQUdzVlJ6bUExOGx1d3Y5emhNKzNrbFBjTHlzYmtpYk4ybXJMYXBlR3hS?= =?utf-8?B?ajIvTTZMaDRXSGY5NjJKUmFhM01UMktBN2g5RlNDYk1vY0d4UHdVeFJjdkhX?= =?utf-8?B?OGFUWEcvVHdHckdkdFg1TUtoVU9BTHJhYUM5YThXYkYybjR1NWRyc1dpdFR1?= =?utf-8?B?MDdqQXJtZExMTEJUL1hsV2xhMEEzaTh0TU1yOC9wTnEwMmJGQVBwZjNWRFZx?= =?utf-8?B?T1NmSVJINlhidzZVQXhLK2ZPRHZRbEJiTkxEZ3VWY2RMaFJpVktnb1RmTTFS?= =?utf-8?B?K0Q5YWtrUjJsZlQwQlU0MEZYZ3ZoRXVLVzhQbU01bkw4M0JRSVIrSXRQR2Zt?= =?utf-8?B?Z3cyRUN1aFBhT0MzVW5zcWtzMEFuekFRaEhKQ2JDZXM1S3Q3UEV0ZkJkbWd0?= =?utf-8?B?djFzdE5jRW9Cc0ZFQU5SN3pzVWhYd3RiNkVwb3o3UGJabXYzWW11cHppUFg3?= =?utf-8?B?c3JlYWtKcFl4eFlTQ0dycDFRQmIwTFA3VjhkTThSNzdncHMwMmhHaTFRRWdB?= =?utf-8?B?bDBRTjR1TGIrK1grMnlaUEJ6emw4OHZkRGRHTnlUVHpoZ2N4U05wbmR0NUlz?= =?utf-8?B?WGZYSUZOOXNHWTN0Y24zb0FPRDR4Y25BMjk3b09zbksvUjVyVW14YmRQajY4?= =?utf-8?B?LzFMaWk2SEQvbVgvb2EyQXlETEc1dlZQbFk1b3Y3ZnhYMzNmc3Q2RkN4OS9R?= =?utf-8?B?ZC9XQWwrZ1V4dE5taDF1ZUgwZ0JwUmdiMnc2ckplZ3RKODhrT2x0UlJVQ0hu?= =?utf-8?B?TVdSSG5nNVFuaEVSc3BlUkw3WWlhRk5IVjFTT1dDZ2hyZGE4VE80WSs2bFNk?= =?utf-8?B?ZWJKMndaV2lCY3R3QnNVT2g1VHk2RlFVS1JnM2h5S3BGNUFidlVmMzFTcFJv?= =?utf-8?B?WHdpVmhTbDdjZDY1dzNVaHlhcDFJYmd1S2NpNnhHdmViU0tTY3FTdEd2d1pU?= =?utf-8?B?SEJHNHJ1NDNIWTM4TFo2TlE0U2dsaDlycFArOE1XcDVJbGJwQlhsRGNWQnFZ?= =?utf-8?B?NVNBS0tyUVJOVjhqdjM5TlRYSzVOS2JobGo5c0pMMnZNb21Zc0VxSjIyeWxR?= =?utf-8?B?MkhhbGRkVm5lTDdBLytkZFVpNlY1L3dmcGhSQ2Q4elF4bDdIWjArSUplZWhm?= =?utf-8?B?dktKNXl4SVQ3NEtlVVRBRjdPZWwxeWFnMTlDRUp2TS8rVnVmMkx6T2swSXgw?= =?utf-8?B?NVNUY2ZiOHA4NitqdnMzdWZ2czkreTJKNjhiNUh5bFlzbTlTSHR1bytPcTBJ?= =?utf-8?B?SXZnMk0vd1dEMk5CblZNcXF6bFVXcDdidWFKcGxGL0hva09pYVllSHJlNnZp?= =?utf-8?B?WGRmWkh6Z2kxRUo3d0NxU1FDT013MS80REdLU2UvZlhOVjZXNHI5ZW1BeWNa?= =?utf-8?B?eFZQenpOeXBuNktmZy9jNG5wUmhiaUtWUitZU3Y0bmdiQlc5T2cycGh6Nzda?= =?utf-8?B?OWtwM2xOamNTMk1zd1BiWjZ0VVFndUs2VEJqdEJzQk8vRUxsQk9MODhBc204?= =?utf-8?B?dzVQbkxQRVFjSVlPYTFMN2lONzl5RlE1SWNhWGh1V3EvajRVWXpmRDNhUktu?= =?utf-8?B?cDlWSmo4NU90SXNBVWZ0aVpZQWRMRE1ST29lY3ZXR1lsR2FTUWJtcE9oOW5L?= =?utf-8?B?Vm9pM0RSZXNPRDgrNzNGZz09?= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: uwo.ca X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM X-MS-Exchange-CrossTenant-Network-Message-Id: c76577b0-3810-4399-53d7-08d8e244598d X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Mar 2021 15:10:46.0113 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: ad93a64d-ad0d-4ecd-b2fd-e53ce15965be X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: VO7V3JZKFuYQPktjXu4E1kVIPkN+9b7OnM3LnkGsVRyiYUzjmzGydzjcPCBezle4 X-MS-Exchange-Transport-CrossTenantHeadersStamped: QB1PR01MB2402 X-Original-Sender: jdc@uwo.ca X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=oTagIX42; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.66.93 as permitted sender) smtp.mailfrom=jdc@uwo.ca 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: , It's great to see this proved! As a tangential remark, I mentioned after Jamie's talk that I had a very short proof of Eckmann-Hilton, so I thought I should share it. Kristina's proof is slightly different and is probably designed to make the proof of syllepsis go through more easily, but here is mine. Dan Definition horizontal_vertical {A : Type} {x : A} {p q : x =3D x} (h : p = =3D 1) (k : 1 =3D q) : h @ k =3D (concat_p1 p)^ @ (h @@ k) @ (concat_1p q). Proof. by induction k; revert p h; rapply paths_ind_r. Defined. Definition horizontal_vertical' {A : Type} {x : A} {p q : x =3D x} (h : p = =3D 1) (k : 1 =3D q) : h @ k =3D (concat_1p p)^ @ (k @@ h) @ (concat_p1 q). Proof. by induction k; revert p h; rapply paths_ind_r. Defined. Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 =3D 1 :> (x =3D x)) = : h @ k =3D k @ h :=3D (horizontal_vertical h k) @ (horizontal_vertical' k h)^. On Mar 8, 2021, Kristina Sojakova wrote: > Dear all, > > I formalized my proof of syllepsis in Coq: > https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colim= its/Syllepsis.v > > > I am looking forward to see how it compares to the argument Egbert has > been working on. > > Best, > > Kristina > > On 3/8/2021 2:38 PM, Noah Snyder wrote: > > The generator of \pi_4(S^3) is the image of the generator of \pi_3 > (S^2) under stabilization. This is just the surjective the part > of Freudenthal. So to see that this generator has order dividing > 2 one needs exactly two things: the syllepsis, and my follow-up > question about EH giving the generator of \pi_3(S^2). This is why > I asked the follow-up question. > > Note that putting formalization aside, that EH gives the generator > of \pi_4(S^3) and the syllepsis the proof that it has order 2, are > well-known among mathematicians via framed bordism theory (already > Pontryagin knew these two facts almost a hundred years ago). So > informally it=E2=80=99s clear to mathematicians that the syllepsis sh= ows > this number is 1 or 2. Formalizing this well-known result remains > an interesting question of course. > > Best, > > Noah=20 > > On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke > wrote: > > Dear Noah,=20 > > I don't think that your claim that syllepsis gives a proof > that Brunerie's number is 1 or 2 is accurate. Syllepsis gives > you that a certain element of pi_4(S^3) has order 1 or 2, but > it is an entirely different matter to show that this element > generates the group. There could be many elements of order 2. > > Best wishes, > Egbert > > On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke > wrote: > > Hi Kristina,=20 > > I've been on it already, because I was in that talk, and > while my formalization isn't yet finished, I do have all > the pseudocode already. > > Best wishes, > Egbert > > On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder > wrote: > > On the subject of formalization and the syllepsis, has > it ever been formalized that Eckman-Hilton gives the > generator of \pi_3(S^2)? That is, we can build a > 3-loop for S^2 by refl_refl_base --> surf \circ surf^ > {-1} --EH--> surf^{-1} \circ surf --> refl_refl_base, > and we want to show that under the equivalence \pi_3 > (S^2) --> Z constructed in the book that this 3-loop > maps to \pm 1 (which sign you end up getting will > depend on conventions).=20 > > There's another explicit way to construct a generating > a 3-loop on S^2, namely refl_refl_base --> surf \circ > surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl > refl--> surf \circ surf \circ surf^-1 \circ surf^-1 - > -> refl_refl_base, where I've suppressed a lot of > associators and other details. One could also ask > whether this generator is the same as the one in my > first paragraph. This should be of comparable > difficulty to the syllepsis (perhaps easier), but is > another good example of something that's "easy" with > string diagrams but a lot of work to translate into > formalized HoTT. > > Best, > > Noah > > On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova > wrote: > > Dear all, > > Ali told me that apparently the following problem > could be of interest=20 > to some people > (https://www.youtube.com/watch?v=3DTSCggv_YE7M&t=3D43= 50s): > =20 > > Given two higher paths p, q : 1_x =3D 1_x, > Eckmann-Hilton gives us a path=20 > EH(p,q) : p @ =3D q @ p. Show that EH(p,q) @ EH(q,p) > =3D 1_{p@q=3Dq_p}. > > I just established the above in HoTT and am > thinking of formalizing it,=20 > unless someone already did it. > > Thanks, > > Kristina > > --=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/msgid/HomotopyTypeTheory/= 0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com. > =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/msgid/HomotopyTypeTheory/CAO0= tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%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/87blbtk7ey.fsf%40uwo.ca.