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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 30080 invoked from network); 5 Mar 2021 18:27:28 -0000 Received: from mail-lf1-x139.google.com (2a00:1450:4864:20::139) by inbox.vuxu.org with ESMTPUTF8; 5 Mar 2021 18:27:28 -0000 Received: by mail-lf1-x139.google.com with SMTP id j194sf1092328lfj.4 for ; Fri, 05 Mar 2021 10:27:28 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614968846; cv=pass; d=google.com; s=arc-20160816; b=AakbiEJpvfVkqKKKFtbH2mDGfRi2N5vSJrOYzka06F+U9y058d84+8wvVxMlBvtTs/ 1s91hpyGYmDcs064b+UVflGDJwTb/8bT0WakqmV6cR4tnBTUQWeBGb3DnozpQo7IrQ9+ 1RbDflC5kvDv8lq1pH+fppi+Qyny9ghZHx4ASQHaYtDa5kyq07Zy8ptXSIm2vqN1bTFy HcrM5htt/NFVNzr33R6xf3dfEk6r+V/mHphSVREvNEP/F8YXc6NMWn2PA74u1bufzlRL btZj6bg7OE0A8PUeJchA1fJtDvBXazqln28iQSpQi0+frqkVFGZKvkcRyGFw40rFBf1B PZhw== ARC-Message-Signature: i=2; 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:content-language:mime-version:user-agent :date:message-id:subject:from:to:sender:dkim-signature :dkim-signature; bh=USfpVhqzMv2YdAUAFlt8eL4oZexWtGP4+aoPfNG3Az8=; b=YzDDCNqcoRV8fPIK2qdiCs7+fWptNNmSdEvuZfVoStrkqyo8GzOWfEPFf1CQT3c9i3 BQWPXkazagRJiErv2XfPDMPN6Lh/SNF/z2l89O91Y2yULAxqS6kyIjVafOiXl5TOBdhK /fHPcDr8wC0P5BVNkv2I8kzaw5FRA0URz7YlH3dm6jBK7yXv5M/OY1Cxfk1sI6giU35q xLGfCPO8G8Wqeiz9ttbeF+cg3AXItOChciI5IVmwRKN8ri+GJAlUi73KXAx1HWqAQzS1 6EfVOPJzmmuXmQIuPuhN+eSwGhXf1sDsGbPZsI0S2qUMphmk4Cc0ITc17iEQ2Z8nE8AP Fw3w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PXnypLCM; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:to:from:subject:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=USfpVhqzMv2YdAUAFlt8eL4oZexWtGP4+aoPfNG3Az8=; b=hxya4llXpkCfqbekpt90FfiQH/llT3ovMdDk07f9bwu70wEVNXpsBHcq1uEqSKW0O9 FisCR3Yk8fQTokHIwi+RsiXm2ai+8QgUT1Nn8J5aES0bQ0JcSOUVCltWlTXOpCYNs9/e MSNKkJ+QCaBTjQ/Yz7KOAdtaIJY4hUq3Sh21c10ZSJ7lDIoshonDZU1Rg+TP+wi+c+C0 jFuc3M73qCpUYU8xUiyXRwrtTzVSjmwbwZ+ABzBoAhfpIExM1FyWe+jRhs0Fgs/hHHKc UroEPQP1l9hNhel0EkaGAmXyi8EuqAPDGYjt2154hKFUffdO3czXKxZqnxCcax0V/EHQ 4Xmw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=to:from:subject:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=USfpVhqzMv2YdAUAFlt8eL4oZexWtGP4+aoPfNG3Az8=; b=TKTznhm7Gm/C50WjPmHps1sKvJD5qGxb+JkKrdOAuz0sNvhGtP8lSB7W56ixljjOAo EMQOHCjGlbtn6gUerAmHVAy1MChLRGkhJY/E3g5EQH5MRVg+Z+jpXW+8hDyPBbu0M35X /Y3cV+IJ+bQChY2YrTKGhrKaoGFZAg8HyKcr4Zmfnfksn9ljEwnv10RZbSY7JWJq52ls fHLkZ2IYH+Cuvezb7TVC8DnPc3uezTpxYYedSSrOiyjwLkeB7gnCvaH0x02Mi6/oXq5G mLYTOHvFblQC0RJH/jqEc13ekV3MBhiuZSI5SdZchMqelrZBqZU8NTWnCDV4kUS8neRc dBdQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:from:subject:message-id:date :user-agent:mime-version:content-language: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=USfpVhqzMv2YdAUAFlt8eL4oZexWtGP4+aoPfNG3Az8=; b=M6F+/Ec5mp/Dzk5NLaHd3Gi7YAFtmapm+NrgGHLN5jlT1wLFDTFAQQIISCq4WoIeK4 9mFp/310VlPo8v66DW3xAqhwBLQ56jxa6BrSRQBX8fq6SnS8h5pJ2ueCB0BXDJqAuxiq 9jEkxTyP1Tr1T6oAWZ2LDjqUJEYyzWmMMgrHdPiLiZfa2KTKlh0SNc6eFL5MAHZPdOK5 JRh31a1M6+W6fJj8nbSFgVK9HgYYkSB8kAeTxSVEHz+VWo0J3k3xsQEHvMI+b1Q0n9D8 ymqvGhkEDINJHTmn4XovCCPwFdKraHxpWyoiWnE3JBs1239MVCArIWVDPkzpOXv6dT9f 6yBA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5307NKCXCxkz+KHOz0rBAOpXHdqVjQI6iIieFxTNl0eX6CPAIrNl cTWizB3o3KCLwfLLM15SebM= X-Google-Smtp-Source: ABdhPJxgWPOBxUQtajqKgVnZOtvbtjF7Ta8luyfKxxlb5OF+iQ7yLpkvh7wN1JuFDTCvca27jmhpPw== X-Received: by 2002:a05:6512:3450:: with SMTP id j16mr6257089lfr.80.1614968846667; Fri, 05 Mar 2021 10:27:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:9191:: with SMTP id f17ls2116020ljg.11.gmail; Fri, 05 Mar 2021 10:27:25 -0800 (PST) X-Received: by 2002:a2e:8e37:: with SMTP id r23mr6031961ljk.269.1614968845468; Fri, 05 Mar 2021 10:27:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614968845; cv=none; d=google.com; s=arc-20160816; b=I7tWrXM5mCRDfqSMmWqyFN6bdDNPsqAmlLWRu3cJjobfYWgw/BVlWXNyh1nTsYmKs1 un+nsH2o09g2V7TbYvgk+w4l2YSUj4PcfS2aYUb/WbL8YvjwFLMz8axgCkAaYqBbg5OE CO1DN7Ks5atH4uRAXM2Asa/4eig/NCrMfy+QyFokKQLYWuTAY9COWjmnMa6WzqHICjoM Q+T28ynfh4l1zh1xMLLqJdt81QIg+NZL0IafroGBDzJiLbCS/mFyG+j1lAaPsMzZU9v4 RMyQ53JmAUW08ys+jCc7zrR0R//sUV8B+UIfUWApKK8w3ijtHkowBSZvJgnEmOLEJ7b6 ZyhA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:mime-version:user-agent :date:message-id:subject:from:to:dkim-signature; bh=B8hf/ozPW9nJ0QEntZ3AIWMc4jRDg43Uj1HScG1E7aA=; b=m67+OkoEmGOu0KNcMtjxPfDZkC+AlcIPfxl6uPUX3EsttfuAJRO6DAhY9GXa2vcNCf poom5rE780AGXmy/EB5r4/1O1/qo9AbWehJhdLT9LGPxUqH3d3bDmJBeUFD3wONpDzLw uq5R3VGFGzJOOqSdHqPOsjPAE60d2Q6ncvXJtoKF5wjIj0WN9uzsE3+J/CgskoTH5xoG m4EdLFO+GRyO2jEqwtT6cq2wXZgQoxYE3d9crEHBe6iJv16dZgUkw0+zP9BnyxjeL4rp tDP7Z07c+QEsRUu57HA87O+nf3dLUAKmPitH55r+82MkqC2RXev6nhjbttNFtGSUfQjs HY6A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PXnypLCM; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x430.google.com (mail-wr1-x430.google.com. [2a00:1450:4864:20::430]) by gmr-mx.google.com with ESMTPS id s5si145746ljg.7.2021.03.05.10.27.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 05 Mar 2021 10:27:25 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) client-ip=2a00:1450:4864:20::430; Received: by mail-wr1-x430.google.com with SMTP id e10so3085551wro.12 for ; Fri, 05 Mar 2021 10:27:25 -0800 (PST) X-Received: by 2002:a05:6000:192:: with SMTP id p18mr10530186wrx.403.1614968844813; Fri, 05 Mar 2021 10:27:24 -0800 (PST) Received: from ?IPv6:2001:861:3cc3:38e0:dc5:38af:f0e6:a974? ([2001:861:3cc3:38e0:dc5:38af:f0e6:a974]) by smtp.gmail.com with ESMTPSA id l8sm5562565wrx.83.2021.03.05.10.27.24 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 05 Mar 2021 10:27:24 -0800 (PST) To: homotopytypetheory@googlegroups.com From: Kristina Sojakova Subject: [HoTT] Syllepsis in HoTT Message-ID: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> Date: Fri, 5 Mar 2021 19:27:24 +0100 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.8.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Original-Sender: sojakova.kristina@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=PXnypLCM; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::430 as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , Dear all, Ali told me that apparently the following problem could be of interest to some people (https://www.youtube.com/watch?v=TSCggv_YE7M&t=4350s): Given two higher paths p, q : 1_x = 1_x, Eckmann-Hilton gives us a path EH(p,q) : p @ = q @ p. Show that EH(p,q) @ EH(q,p) = 1_{p@q=q_p}. I just established the above in HoTT and am thinking of formalizing it, unless someone already did it. Thanks, Kristina -- 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.