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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,NICE_REPLY_A, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 6467 invoked from network); 8 Jul 2023 13:16:09 -0000 Received: from mail-wr1-x43d.google.com (2a00:1450:4864:20::43d) by inbox.vuxu.org with ESMTPUTF8; 8 Jul 2023 13:16:09 -0000 Received: by mail-wr1-x43d.google.com with SMTP id ffacd0b85a97d-31443e13f9dsf1562316f8f.0 for ; Sat, 08 Jul 2023 06:16:09 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1688822169; cv=pass; d=google.com; s=arc-20160816; b=Uxp/3fdhAqu2yRdzKhjxMza0UtZ95vOXkCW4Sh7y5KiN8LFvfKen2x8C73syGQCXMO V1JmicLjsq3hsOBeD+e/eHkQkiLdaQwmaHsppyvxo4KthI5xNPrzC8A+hdvHIPr8yM8l zheys9lTWG/NvwQhQFLuSRxZpbtfte7ezXOOasGxegi7kuKDvZLCFhQTVSZyv/vfhqvw WhnVSHM1X2hFAbcxPs4u8Qn7Bg+LwPbOa3PsF8Z/5FclfrQ9mQYUBbXrJyiKgV9uytYG //IbUxJMrbpMrxATueKVVaBJ56rDS7R9dSxGQa8rYCT/nfQNr6m5dmXxrZvy1HViF7Pk J+ZA== ARC-Message-Signature: i=2; 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:in-reply-to:from:references:to :content-language:subject:user-agent:mime-version:date:message-id :sender:dkim-signature:dkim-signature; bh=zqEBISgLMBLgwP/omI7znL7yHbJmRAnDodcN5jZw3tA=; fh=IqGH4qO4F4wxFST53s1mcDspaLqdqgO7SE9VX4Kajtg=; b=vY0DYgfUvoY2kW4z3t4FoONs2rNRtb+VVY2OT8ig7Yi54GXzNxppYNbJGLDoSQ2GzU UVUInw0SWWZ44sZXOYjYii8kD9ByMe3YTIwplijvTbp85s7Cme2a5TfbCzAzJTtPI58t W2R+OwBU5mux13R8gQlbdxbbqMzqsf+wcRkqIpex9FbjmSqecXT0SRXLa3aJc8vlqNwb Kj22js0iDABzEjpFmd97SfmHIIKr1YdtuiQ0FveH4Ch9G1jN+AT21oFxLBL0CSCV/YWO yDm8WGOIehKql5zfUNpAjT38NuUiBlb/PV6LoMcNE/nLTSDEiuwygIBlNjwpwJ8+BQ1f TUyA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=pltk8hHa; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32d 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=20221208; t=1688822169; x=1691414169; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:in-reply-to:from:references:to:content-language :subject:user-agent:mime-version:date:message-id:sender:from:to:cc :subject:date:message-id:reply-to; bh=zqEBISgLMBLgwP/omI7znL7yHbJmRAnDodcN5jZw3tA=; b=OuH/EOF6nuJ7pnRa9iCS7Bh6VnnDqRPcmnQh44Ef/AArVtSiJHoQFPWmy/OayZZnA5 YHQB9ddAFH9k2KqWVcG5qH2qc9NJhctjdMifdCJIdA86cRUr5QjK9CpXD5tPLIGtYm8L 7pqBebtrx4zZjslBjoPReNA70DSHcZu/0EywHgNDb9v1cHqrUifCsus6JFF1EIM32FyM br65Z2ESvCKUX2LTQaq7VHvbVGPUoNz71zJvnzZMeDhsKNqcjnuCKI8MuCZGWAxbGuKw H2rE6101KpIegP2rqov6pXyf85/lyIWhpuvFdMM/OsSJ3yoAGFFwGtkxrROErWlqQljX DyCQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1688822169; x=1691414169; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:in-reply-to:from:references:to:content-language :subject:user-agent:mime-version:date:message-id:from:to:cc:subject :date:message-id:reply-to; bh=zqEBISgLMBLgwP/omI7znL7yHbJmRAnDodcN5jZw3tA=; b=Qw1eDLPKJGghPuizBF3kdACVmp+pTVmZc34NQD3iNsDFnKCyCGb924iP2SmURqcnwf bdil+U+n8ussfkbWtfFIDy7JUfozqtcLeFHpYM9hrhuda1tj3ltykNJzAH0x09sgsuzb bsea5fF/9OzLjeVTwS2wicSvRZUF8+NSSc+vsvaydyKdErGm6nGtprFkd8Vo+Mjeq+R0 MByo/+43gyqVh+IeGIAuyIMPm+Hfj6Do09nALPhMQaRNi/Rxla7ZmRBdL3xH4l/hggX3 Iun8w9lLkfUq6P3ZYnCfTtDj+X/i3qSvIMm0vhdBosVEaQlHqRfA1VAvAWMJyyL2as10 I1MA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1688822169; x=1691414169; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:in-reply-to :from:references:to:content-language:subject:user-agent:mime-version :date:message-id:x-beenthere:x-gm-message-state:sender:from:to:cc :subject:date:message-id:reply-to; bh=zqEBISgLMBLgwP/omI7znL7yHbJmRAnDodcN5jZw3tA=; b=Xwx508Tw0oujmt1BrL7ZRhFIigE0zWw/FbIi6AwcfwFPGn+jwBSnaLVeSghBbfaBia gJRPJHlJ5V2DuFmvOcdcBX+vhNH5K89TFO5h3ySeLfgBV+2n8cf54Tct2B4KoEH/dulq kmReYUwFgUc0FGvOZiQeH4Qo+TIT5VbzD+yn9lwm+J6S9a4gfDU0D9p8zKcXJNxYlDJV uj6HN8SCxUZdmcPo9cuZIWQp4PWqvxknJxVdh0m/6q6PdwwlT2588BLkAHXOrRapM+Go 1QpThj8c4HrXDRk3rzVxOj/P+hCKeR6hKH2SSSGhu4NoZt0fymY3p6jUfkHoYnHLlTAS mX8A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLYexLFKoBYC7ZySpV65JusAI3zenmdPkMjVbPnN27mZyKI8aSYx lWBod/N76vaYVsg0uB3bvds= X-Google-Smtp-Source: APBJJlFD/ouWEk0nOY4ZORBC/eW0av1ugOb+DHvjGB/NaCOqs+plWL1rIRMPZnq39fXymgsmpaaH2w== X-Received: by 2002:a5d:5088:0:b0:313:e553:b858 with SMTP id a8-20020a5d5088000000b00313e553b858mr6112051wrt.33.1688822168504; Sat, 08 Jul 2023 06:16:08 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:690a:b0:3fb:ad1f:200a with SMTP id fo10-20020a05600c690a00b003fbad1f200als1374665wmb.0.-pod-prod-01-eu; Sat, 08 Jul 2023 06:16:05 -0700 (PDT) X-Received: by 2002:adf:dc09:0:b0:314:3724:6fcb with SMTP id t9-20020adfdc09000000b0031437246fcbmr6172241wri.50.1688822165714; Sat, 08 Jul 2023 06:16:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1688822165; cv=none; d=google.com; s=arc-20160816; b=EGf8lXIzSCWAgPE+lMONQVPqvFytzGTbHiQLNfOCy7IwOtI4e/5IrchaLu5GEEGYP+ we7Z5JcQ2eI++aWeiIYm+scphlyJ1P4khPIsxp3TTBJk+HPpyMHW87Xw3L38KnwquLiv rEShhXL9dz4g9m1xV8jJMrfe2JcIuS2IDHsMbXcMZ8i0NnhLkQ/VJ1C3g99l33HWk8hP ZQEdLSK8jDA3/HjXw3H6yL4xqzAXMPXV9NEH5z3Xq4lHx2ApDGBfQ0TXeuNzSWl6DYkG w/V7OqZ9dcfFOf6/TUK6Rr4jHTQNu1mulxq8THdYVKYZ7GM/8z6VAHm28ZL6jAV0I1Db V6nQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:in-reply-to:from:references:to :content-language:subject:user-agent:mime-version:date:message-id :dkim-signature; bh=Tj2uFxNco52375VikAEs6O1f+rSWLr1dFTUkVJP6y1Y=; fh=IqGH4qO4F4wxFST53s1mcDspaLqdqgO7SE9VX4Kajtg=; b=XpbKwA8a6uK8bQNV0ruQ4qY2lFhb1HjOuVuShSjpsTt0NAhaV+yTlwFdgdKVMgoQzi 0j2abtdfp4TDZnk1ydTfr82WoFdrp3zCMdRfAIaSNGuYflEdXKJkQ2H+luJ0JQgwyEtP PfYp3KLskHK8HwWO0P93yRU4/f5gkG5cEjuUS9atILeIfjGovBrcrW+D2u7UNEbQoEBR uzQdllCU5qGBwJQWg7HPPkwcGNpByiD8pCDVrn6bnhXB6IURea0WLBDYbsoRkiwmjnMI uuvt6pxEC81DmQwr2tY/29O3obnMzEKnOtC818NCtzNvebhvMqDjACEZ0wT37oiwZ12r 9ugA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=pltk8hHa; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32d as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32d.google.com (mail-wm1-x32d.google.com. [2a00:1450:4864:20::32d]) by gmr-mx.google.com with ESMTPS id e8-20020a05600c4e4800b003fbf22a6ddcsi295496wmq.1.2023.07.08.06.16.05 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 08 Jul 2023 06:16:05 -0700 (PDT) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32d as permitted sender) client-ip=2a00:1450:4864:20::32d; Received: by mail-wm1-x32d.google.com with SMTP id 5b1f17b1804b1-3fbc6ab5ff5so31653675e9.1 for ; Sat, 08 Jul 2023 06:16:05 -0700 (PDT) X-Received: by 2002:a1c:f713:0:b0:3fb:adc0:609b with SMTP id v19-20020a1cf713000000b003fbadc0609bmr6416166wmh.13.1688822164533; Sat, 08 Jul 2023 06:16:04 -0700 (PDT) Received: from ?IPV6:2001:861:3cc0:bc20:91bf:d689:8c3b:38bb? ([2001:861:3cc0:bc20:91bf:d689:8c3b:38bb]) by smtp.gmail.com with ESMTPSA id 12-20020a05600c020c00b003f819faff24sm5167452wmi.40.2023.07.08.06.16.03 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 08 Jul 2023 06:16:03 -0700 (PDT) Message-ID: <8e549102-49ca-407f-e95f-22d971f4b9fe@gmail.com> Date: Sat, 8 Jul 2023 15:16:03 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101 Thunderbird/102.12.0 Subject: Re: [HoTT] Syllepsis for syllepsis Content-Language: en-US To: HomotopyTypeTheory@googlegroups.com References: <5255bd6d-8b20-a4e5-bc6b-4f8418bc6700@gmail.com> <1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56@andrej.com> From: Kristina Sojakova In-Reply-To: <1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56@andrej.com> Content-Type: text/plain; charset="UTF-8"; format=flowed X-Original-Sender: sojakova.kristina@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=pltk8hHa; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32d 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: , List-Unsubscribe: , Dear Andrej, Indeed, my message could have been more user-friendly. The file contains alternative proofs of Eckmann-Hilton and syllepsis, together with the proofs of the coherences described in Section 8 of https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf The last coherence outlined in the paper is what I referred to as "syllepsis for syllepsis". Best, Kristina On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote: > Dear Kristina, > > any chance you could spare a few words in English on the content of your formalization? Not everyone reads Coq code for breakfast. > > Many thanks in advance! > > Andrej > -- 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/8e549102-49ca-407f-e95f-22d971f4b9fe%40gmail.com.