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 25742 invoked from network); 8 Mar 2021 16:26:02 -0000 Received: from mail-qk1-x737.google.com (2607:f8b0:4864:20::737) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 16:26:02 -0000 Received: by mail-qk1-x737.google.com with SMTP id x11sf4462956qki.22 for ; Mon, 08 Mar 2021 08:26:02 -0800 (PST) ARC-Seal: i=3; a=rsa-sha256; t=1615220761; cv=pass; d=google.com; s=arc-20160816; b=p5010NJlAqEP3PiIxklHj8dxPa8N13+DK7BBQN+Aww6F6+CYbnrnAKNwDbwhwjx+W1 b4nS4DLxLrZorSChTV5/oQW2WsT76KAsrOugLKyDsJhOoMhRscpx0xs7tkZsX3IdD9IP 2rLinNFOAT2F6EuUl0jeM61aOXsbQxQ4BgPThtqTinugstcwvI2a3uOfuP1fGrJ4Vesa sPnl/T+iYSBxTFrxLFT8y43eOZCTVdyRivwxN2DGJFzc9V1NJaXs5KDMAFJ1UKnIlqIU EpJcFZdTGLsPZ86k/bc9fb2D/rfzKOjl9l1U8zQ6jwe6l0vW3zxxHZV3fUL2dxGeBwcu pn9A== 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:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:sender:dkim-signature; bh=zZAQwlLU1GXzlXGoN2rBuzw307KzSA6S4bq6pRCDcww=; b=m27f0lLPm+4uRfLFQB6sN35Fm7bsoIIdWQQEungKEJl76ayXRL4V/kFJg26pIGJaPb Qb0mW8646hGfyvoQ6raL5B68sNAwcB3X6LkjX8A0DM6m4DgshgJ7F/GoJkJBgTIqJScl MKl4lGkw2oG9MBlLIDHzB6IXkJXEynmoNRaI4UL05h76jt8GAgM8CF8r+PjvHsSLs0zw cqnnDhAwAadHPAr2/rJRYUdD6WwEvZ+2U2dXZuF20ic+Z5yGVWqn0BfXIKqJOCjDbic8 rz/0o+E9MeqUcLaQDxk0GdvcpOFYmTuxd5nWh43AgGM8sY6ZunqgaOSqZ9+o8CcmJJlI lnWA== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=EpM2WeJA; 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.138 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 :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=zZAQwlLU1GXzlXGoN2rBuzw307KzSA6S4bq6pRCDcww=; b=bZL4+AdfFYSvp4s1Ve50Zr99xXrvUHbfefllvsxTcBqEhQ8bOHUFOTHQeqFlDxCkTN 1TcSfVhiWKzcCmj158V0nKRI+D2eL4OUn1d1g2fiQ4A2jTN7tZ4OrTmbVAoL3d+0dnlG GdSZ6Au7vtgl0SxUIbHJMGmkpvbwpaBU/3XsAEmav+KPT2w2qYTvCft/NroelMqvwm5B odyhqi4HzUIP7tKti7TP2U7D+PTowvMMjzEI7Pwq1T3UQ1LX9OKs+I2mj8BnXjZQ27rf usjz3Rnu0pTgw+eIcdceJBNc+W+reZ2wgkk4HqM5eObNfQsBJuoIrBK3arjff91EAkUk 6R8Q== 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: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=zZAQwlLU1GXzlXGoN2rBuzw307KzSA6S4bq6pRCDcww=; b=YBTUY5NvNIjm2J1ttyEncFEyTQwT4vgRTXGvDsuJkFcE+j13PvfoA88HR1USH+NZJP aQSbKxLlvD19UIqzcXPBeX6FdWaVqx6zs70dsbFnc40KSFsTOJ8auHa0Mhr3rqIYpV3e ogvA9v7p/VvhEVUQwAZjZDf83JnU+XOwDlkRtgOvVKUoZcMiWQtCRo4JpfO+mGEoOqDS ePomtyl4XGS82l3YM6l8yfG1mdusBwbnotVB8ihsGGAkH5Eb+KujdaDTJlq3HFolodNV 72LGm2GDnmKEa9b/888Wl872fa/sT1MRAMTVR1tABdsJ0RTS+mjFtXmKLDje0ipJln39 4oeg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532Jipqc03IB1RQwQp+h4kWiwCEfbER46/jGrpGybIyQixGU8TKW nz7n/AtQr4FbUhEsfkuB1lA= X-Google-Smtp-Source: ABdhPJyTN8h/X5vl104s3/qM56eSAWbXh803MKGCVHV05/L3fBQlVq6ZW5VhI/QE0QHLHn6QFxayEQ== X-Received: by 2002:a37:4f49:: with SMTP id d70mr21122791qkb.353.1615220760997; Mon, 08 Mar 2021 08:26:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:d8e:: with SMTP id s14ls6859941qti.7.gmail; Mon, 08 Mar 2021 08:26:00 -0800 (PST) X-Received: by 2002:ac8:1116:: with SMTP id c22mr21613023qtj.230.1615220760466; Mon, 08 Mar 2021 08:26:00 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615220760; cv=pass; d=google.com; s=arc-20160816; b=r7rA6qeJPFkxqi/SCGECJs4Wx64Us+FuEgK521Hc3iqmIhQJyW+wMGnT+WTI0TpI5C PK8gB43la7/zZutjOmIyJu9uVwEentlQgZGMCe9LxBJsFMeYGHPdS31BnAucJNM6JE3Q GFHG5+C8oR/TdeH3LwXeRIwb0+nzweQ4Xt3CTc3EXccwBq2bMNDzNb5z8j0LyfMPe8sr vsDabgn6wRfN5ZvKQlUjqbV0BuP1a377GUlqyl2o96SDLTjr8a1EmUqJqQyn+0BY4JyE zpPr+u1u8KHvFz8Gph613SsjAAv4Ggvc2zjuylz1FG2IMMpSjSHA+STVNm3q786+/y/r gYzw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:dkim-signature; bh=YzsT+soztjXQWQ2hVHD6AEKUUGVyGiUn5kWNpDRQVUo=; b=jWUfdo2IQhH+59xkovdYc+Lal9xwRBiQMWfLs4VMVxkTJJ0nkRYC4K4Cp9x2ERxgMR VUVKv17w7cDrDTx/8R7pej8wnVbGtsh4K+c6o+6i6bnE3R+/N/d6TgFZovRZHGeEjEEQ s/vXYEVfkQ9UUas7bXkpMQyL7u887oZBaO+Bs4alixEQsQAzVj4s4+O8/hUroPzQVUJG d73mpf+odn4ug2fQfQK6hTl2HLreukarJOTP75dKKHDo4cI4TduUQwNrB4VxYs0dbmA6 i6pZ55GxP6e5+qf2wJ3SqNqer9F2q8jH5J3cKs8oiBbxfyt5c8kDVogzCdKS0uGiC6II C6wQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=EpM2WeJA; 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.138 as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-QB1-obe.outbound.protection.outlook.com (mail-eopbgr660138.outbound.protection.outlook.com. [40.107.66.138]) by gmr-mx.google.com with ESMTPS id m10si413912qkn.7.2021.03.08.08.26.00 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 08 Mar 2021 08:26:00 -0800 (PST) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 40.107.66.138 as permitted sender) client-ip=40.107.66.138; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=WnTWN8qz5BRkGB1Fc6fjhuPOPbKQptehkxn4nJOa7rxjtH3WZHXvqG4VVM//bpsyGxQ/sQ9JxmALB8TXJXcl8rLTYWgl6D8I/t+8MxfffF/+4YU+o75bMvlwb49nkdTxKMw0GdkUSBMji2vmqwO6aAHa2GzP3o/rJC3Q0nYPfaMS96rXbJkEIHlH0XYwyDwLrtkCmxiL94nRTCu7HWg3F7pR2M/zS5qAqCPJJaLFIshwjHTFkvGItxrO/m14qoq+VZrA8B3E9bK3c4sMamfThU/eeXa9uYzINFUxRYfQ8L7AvfTXfiZnR4Uj0BVz7UJTLYAPToWfe54w46oQCL9T1Q== 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=YzsT+soztjXQWQ2hVHD6AEKUUGVyGiUn5kWNpDRQVUo=; b=JqpxX8PphYiB3RrPNRqHJKd5nSyjZwMcXWGBVaNkSNgGlOuhwFJNu07CQDU++hzrNtZZhGJMhU+cGPEjMdz/n66BcL2efZvMk1w2SHNP9fkQlgrq0xhcaqJZ3LFl4qtq640am+uUerfl8/EtaiF5K+QXRhX9eKVJq1+9o1myfte5VLdMAGdh74VrRi3CfWEuID5gw2c4TPrbVWgaqfOhXxa5+8tDZ7LpWRiEU1YoztiXZgWeAS8gOLgKXrdcO08dVDEJXzGOC3v3NQdmYHNT2r1ZwD2FcelXPnHsCDYbkVExykf5xY7x4PaJQdT4HTi3UgwJ5NyRezUPnlH68k4fig== 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 YQBPR0101MB1681.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c00:12::29) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.3890.28; Mon, 8 Mar 2021 16:25:59 +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 16:25:59 +0000 From: Dan Christensen To: Homotopy Type Theory Subject: Re: [HoTT] Syllepsis in HoTT Thread-Topic: [HoTT] Syllepsis in HoTT Thread-Index: AQHXFDe4fMpeDKwvf0SE+i8T8qr10w== Date: Mon, 8 Mar 2021 16:25:59 +0000 Message-ID: <87pn09ipd5.fsf@uwo.ca> References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> <7d4b6fd7-3035-e0b9-c966-97dd89d8b457@gmail.com> <87blbtk7ey.fsf@uwo.ca> <1f7bbcb8-ee50-0c24-174e-d3852e52bbee@gmail.com> In-Reply-To: (Egbert Rijke's message of "Mon, 08 Mar 2021 16:46:29 +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: 06059fed-ea86-43e4-8be4-08d8e24edba6 x-ms-traffictypediagnostic: YQBPR0101MB1681: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:6790; x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: FiAv0Ss4PlS+4ryavsWckatzXSaLz3AX6/c01LgzgTjL8R/mec6tfxIMHycj0EzOt8NVxgvq1Z9fPzchqba8RJXmRWuHgoPaTqCclc9WT5Fdizn8iYP6pOuFSue7vaD/slqzmUmOw8PifdGlao09ZWGe+ozOQDDGh/kHX/DuyHir9OUK/RccDCrWa64I4cwd6a82//DljtK3tnZurd7q1TNgI1l7f50lVtCQoprGzRVkY+GVqEHFELC9YbZswUFuGAaz9Z3CRogHDsye8PtXI7N0JRif9QMu9/VINKxs+WlrFHSAHg1f5J2yZEsbqNVPFcB/XzW8L75lnuY7vtic4k7+YSsJSrBbdi7A+DdPWiDtPw7n08ALJJIM5YJGzG3itonrP8dKS8ptzg+APcJ45QPo1UX6ik0pLz4LQBj/Udw/+DwEET9E+sNkK13dVV9ktdbVfs9cywrNn/NaFNqWypbxV4PNmGa97QXI6Ga0e9Hi251XHpyGZqsyX3ARvIrw6NrLf9LUVHg4D3S5RZrOzPMt3iDw57DTShG/ckcLX5y8kjhqXaQGwjIvoxdNvyF87uiRCGGWzlW3Lw+d1UYr4efJSOwCKHK0vFD+BhIZjfI= 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)(39860400002)(136003)(376002)(396003)(366004)(346002)(8676002)(2616005)(86362001)(6506007)(2906002)(36756003)(6916009)(71200400001)(4744005)(26005)(186003)(6512007)(786003)(316002)(66476007)(76116006)(6486002)(5660300002)(478600001)(66946007)(64756008)(66556008)(91956017)(8936002)(66446008)(966005);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: =?iso-8859-1?Q?4WJ5h0Sg5ThpteL8rKlpM/u1Fawiw8juhAfnRO34HGAruQa2yHpCTH/QbK?= =?iso-8859-1?Q?hOCKj9jF5LgN3Rv83jpRKUFTt9LVee5sx+RS9NLZjrO/OlIu6p/8DKtdsn?= =?iso-8859-1?Q?S+S70fU7s2+WRQVZXsTWrEJKrThhbD7NDwU3LQYhXgaNMGY6giyJyIzSNI?= =?iso-8859-1?Q?Z5QYnEX8hwUnpoJ9vYWtsUVAjLmnwB7O9pLeTDjLcUI4YDVMXLyxtTFmgS?= =?iso-8859-1?Q?3Rbbd/nLZDoDLZEMgls/+NDeZb2jZ8w3MVYY9xfEL/w1h7P8fEXcuPECLz?= =?iso-8859-1?Q?j+tQBZFSD2vwJkGAXAqtuFMCbzEpbedpG4+/eV7oaiGhkpDvCqg0p/xm/L?= =?iso-8859-1?Q?QI7MQqd47gI6w2qtn0lskk0TUZmzZmYnvv1sK77tDjkcbh6QlOJ9WgdIgh?= =?iso-8859-1?Q?LtsTiy/2URzffaxCsXK074k/qWl+wT3z6+aHPD+fnGwLDeSmX8H8evruUz?= =?iso-8859-1?Q?v/UP6G9WrO7zZl7PMo7ijd7rF+r41sAho65MlRX4BV3LDs9QeAYkamLLqd?= =?iso-8859-1?Q?pPhIZA5s2EIJz/GVr3VT/oVxc6SjHfwR6cC/zoFWBAiyAyAaWhuJ7bQOuX?= =?iso-8859-1?Q?3vakYiNCdAQmQLzaBDMni9p93VmalsBY/6MHArJUWddxcQDUbF+gxtzClZ?= =?iso-8859-1?Q?9H0f+efzp7rtMsWuyHszJEoJ8e1ayvawuMzn9PMAvtihwWgV16QUCeWnI7?= =?iso-8859-1?Q?srE36eEg4MSZ2KWQbHh4TXRzJqVLItAWfdm26a6Oq6b0eWTpAHDmQf3EMf?= =?iso-8859-1?Q?uJ8RBudbGzHKcTl69Jb5OJgNunjzJjy1t9CHEaE0+GpbHSHHSonaNdq8e3?= =?iso-8859-1?Q?klls2s7yfOszmObIzFyRw7cB5GKX0MjFWyzWMvpsxycnvaj70pYvRgGU2i?= =?iso-8859-1?Q?wcTv6caRhPf7qojs20uK5U7MVEnx3TqkLIjR9SG7mYT8KtNq84mNMxQPmy?= =?iso-8859-1?Q?rxDclXYNdh5IpMi+YjMPOwHrlSPyiRhoY/i0mMI3V1kUdVSu7CvDuTuvR/?= =?iso-8859-1?Q?WULcO4zgY+h288IKTtaqJ9N54nYPNzhcoE1CbOOci786t49IPxjKUYerwj?= =?iso-8859-1?Q?3Sk/0KSPXyIhzD7cuQIwTG2MFILVL5FwNg3oa8K6dOrVkiG5lvcQ3e3PCT?= =?iso-8859-1?Q?PwTcXbKn90OMAS8IsNEkgZB6ezIyhff/2YiP9xc/7ARcHV7Yf0K6QMN3j/?= =?iso-8859-1?Q?1QzJE41VVqwM8rVzTC+5yZC5vBwJ5E90hZWNrgM9sc47f8kxoc9OMg17TW?= =?iso-8859-1?Q?G0cjIKpyk0luLQs7Orv1R6pTXXJUQCsc02EUKOgaQwUl7qzJDAVtzK8jWY?= =?iso-8859-1?Q?BvxGnBcea/6o613JiLq00/On2IWYPokDFuZbc6FdoFLkslVeegzMr8U7tD?= =?iso-8859-1?Q?O43HKu58yK9ZADcUP4KC2sR/fUycEo/g=3D=3D?= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="UTF-8" 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: 06059fed-ea86-43e4-8be4-08d8e24edba6 X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Mar 2021 16:25:59.2067 (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: OYOcQtH+T6cdNlkQjHAu23fOssZcFt90/HSLTZ2io9m9amzIDjvchFxTwleIHCO6 X-MS-Exchange-Transport-CrossTenantHeadersStamped: YQBPR0101MB1681 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=EpM2WeJA; 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.138 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: , On Mar 8, 2021, Egbert Rijke wrote: > I had a different route in mind, much less efficient. There are three > kinds of concatenations in the third identity type, all three pairs of > them satisfy interchange laws, and there is a coherence law between > the three interchange laws. In case anyone wants to play with this in Coq, in this branch https://github.com/jdchristensen/HoTT/tree/Hurewicz the file Smashing.v contains similar facts, e.g. pmagma_loops_shuffle. (But no coherence law is proved.) Dan -- 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/87pn09ipd5.fsf%40uwo.ca.