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, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 3736 invoked from network); 7 Jul 2023 21:04:25 -0000 Received: from mail-wm1-x33b.google.com (2a00:1450:4864:20::33b) by inbox.vuxu.org with ESMTPUTF8; 7 Jul 2023 21:04:25 -0000 Received: by mail-wm1-x33b.google.com with SMTP id 5b1f17b1804b1-3fb40ec952bsf12745145e9.0 for ; Fri, 07 Jul 2023 14:04:25 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1688763864; cv=pass; d=google.com; s=arc-20160816; b=TRfth6rj9vO0oIEDcIx9obv/g5EWbpWCcP6DGq33fN9Pg1/lW+qgqLCLtN3PgZ6g6g 1gJLulqQzFJY5xOkb+SBhImG40CRRNabBiGeaUmJoB7NUMXOeJJBJrv7ESO8ifaoR45W zB28QqgNO/XF/3u6tztLc5qP7kvREr84RfWvhbsXA+C3dupUr4JslgG2Ahlgy0nj6W7a MqXCIQzdYs1mMhv6e4n532MjF36n95mu0TB3+AwDpV3GjTvFsia+nzLLe6M3jdPkPrSj 7ine2ls9uAYPK4fK1wHIR3wqpyZqrWYfdYRLdVzfdY6NZBXVc2rpzCp98zYH+SHsLASO roJw== 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:subject:from:to:content-language :user-agent:mime-version:date:message-id:sender:dkim-signature :dkim-signature; bh=rUQzIHklDZ7RFFgZKgoQ7gXf/FkILiriPh2BRbZPNXQ=; fh=Yn4Rb6IEHIo7kscAwj7vxldILG3PMErAsO7Mzv6kHsw=; b=RS+SuRIYNBgjqZ17yVHZCOVEpLOL2VNifvnYfH7sIiFQarCHE9szIWuuKWZC48YPtK vgnX0fuorOu9KaSwkh1h/Ap27bVud2g/oFKkAVMH5KSl+QfFrleK++IJO56xjUCro3t6 pvqBPMOmpC7xXltBpJY8xcpYC6KcIRJFyFuuajeqZRwjgCO6qF/v+zABm+gxGGqTyNo2 +u3JJUvRaiU6ZJlKaSeRysbKs0gTQqgxvceiGb75pllNJnNECSWXu9BgLVqqqva4BafR si6bU51f1sOKKr4064w8NtEJTHK6Ezzt6yBz/fcorJsJgD//yqj62awwc6sCiNiqEiEd gTHQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b="g/EGpEz8"; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42f 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=1688763864; x=1691355864; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:subject:from:to:content-language:user-agent :mime-version:date:message-id:sender:from:to:cc:subject:date :message-id:reply-to; bh=rUQzIHklDZ7RFFgZKgoQ7gXf/FkILiriPh2BRbZPNXQ=; b=IrpXdCIjgzz7MI+arMY7kE58WlQecc9cWRduK7nS3/N1/zhNsYiG89iVm1zf1mG1c5 7ysiexnl6GzbAWLgf8/L7K8r1j5pxYtrKJKu59O6rCgiUkepJmRZOqoyoWzBOnHRjsPm 0aco6CkaCkBLVAzexD8zN5clQVqzCNVBKsALbRYN8bA0Sq4oGbyVgx38QRm3dEhoGk+F GZOAyrRT/nHigKgCa7jk9yEj2Iqri6jAdivIjSCUsS9f1qaE0RvxeA/rqe7XUde/TP3m k6MdBsX0xFIotZrlfshlGQheXX4pSYwT+Ys2XqvaonFPPFCC25Og5G71pEG133PJVDQ3 mAog== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1688763864; x=1691355864; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:subject:from:to:content-language:user-agent :mime-version:date:message-id:from:to:cc:subject:date:message-id :reply-to; bh=rUQzIHklDZ7RFFgZKgoQ7gXf/FkILiriPh2BRbZPNXQ=; b=ryvmF3RxlyRRHGwNw7+vTJCIT5+wloe4vM3TuhBQyH+vk6k57Zu18z9AzKQTlFce6l qKQ2qv5Fevj8FB+89S7D84Tv1ZPRHakF3IW0nNcRlzXfFLKkOvTt7aJtxGb6HbDS7AHu sBYdWogx6ZjH40FcSDeLmRMG5hJdD5DYKBFHpjukfhiPfdwzK4NDDSjdL1zGOr6+VafI 5CchNZCmNiTo4MsvkGoIJV0bElywvOPqACbOgpgU55Co8LN5anitg7b4DCj3gPkGisL2 bcQoAf+fTvYsLYEqJqdS5y1HNcyFoSNU1cMHneWen97Zj5iokt5AElG2GG6Als0y5l3Y GV1g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1688763864; x=1691355864; 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:subject:from:to :content-language:user-agent:mime-version:date:message-id :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=rUQzIHklDZ7RFFgZKgoQ7gXf/FkILiriPh2BRbZPNXQ=; b=ctWoAHRBfsOcK+UfCO789iXO60cqzL86k+4vSTZgZRMWOdBg+if4xpkK01tUb6PtMy KH469L+546vUMkuFvVLOTIcZcyK1w9e1YYMqTIVJgB7yFbGhlYHE6voVqd7Ox/qs/VT9 w60AK41eC0tWVWMW46o7byoR1FdlDK+Fj2/dy7LC9HZUt1CkoL/pHZMW6ZS8oJ6xziNP kQdOikFlsvFpxAMVEdHCAd23QatQE/HjXenI2UoWxtoJJW6rH9ySph++gLc6k82gbXDf rFqWUeWhPPZiqDNPjSty0XQJT1MYE5HLFdp+oFqOKLabEz859XRWO0bgAEvSaKgay1+5 UitQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLY729qnxUSxuBi3a+jOa8vGo7BMio/J2iaIv8g+ZfO9LNYUMnex EV+013hm0v0ByieUSx46A2M= X-Google-Smtp-Source: APBJJlEACBVYe6xRPiRCtLDgVflg0nzteQTwRVh7Yj4wKAjOVjvlKrgOEFHDlUXxf0zLAieJXj9DRw== X-Received: by 2002:a05:600c:acc:b0:3f9:b30f:a013 with SMTP id c12-20020a05600c0acc00b003f9b30fa013mr5179163wmr.6.1688763864236; Fri, 07 Jul 2023 14:04:24 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:690a:b0:3fb:ad1f:200a with SMTP id fo10-20020a05600c690a00b003fbad1f200als1121439wmb.0.-pod-prod-01-eu; Fri, 07 Jul 2023 14:04:21 -0700 (PDT) X-Received: by 2002:a5d:4b4d:0:b0:314:49d2:aaab with SMTP id w13-20020a5d4b4d000000b0031449d2aaabmr4966981wrs.8.1688763861364; Fri, 07 Jul 2023 14:04:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1688763861; cv=none; d=google.com; s=arc-20160816; b=DtmT+sJS8MaEBkl0WNWL5jI7utnh/b4O+Dhn0O6MX37wjm3pa7bxiHyZ2qM6lI29Ow mhoOWBYSaCwAPTkI4mtn3qJHEB5QAo3JnzfM8RXEFt8WGRN8I/t7rNmGbQ5OcjNx5mHz jTGg+U5hvtqTXoOzadRTmTwTUXbyespnzLZUqIQ1IAiZYojJ/hr9cWTVDnEPLdrnSfzh LeYvcplbGvCi1sLb/1pBQ29PXtMx/uLnR3E7j4qqrSZUELLYbFh5s1gyQ5lzChTYYZzc IfNLkILAbZ7PBpHjccW3aY66oFwYpGIgbtoO/Wwuogqf0XkkDmfHFWYkF56jLDToRZ7k NofQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:from:to:content-language :user-agent:mime-version:date:message-id:dkim-signature; bh=2qX1Taxc8uPr9WpN0AhV6wdSk0tgZ0R0p4Hn3u3HmEc=; fh=Yn4Rb6IEHIo7kscAwj7vxldILG3PMErAsO7Mzv6kHsw=; b=LhHcvmT8KOgB2RHbrbq82BQjag8/KPhsXEKgUqkM3avl5DH1L0j70X3y9aKHX9JeQZ 61CORzBrqkI4GPWC7uzHsCKhD5K1/h0O2ef6hqr/1fFoENiYXLuxKLBgXTFNJLJ6GSvD P8Qa26y4+nOI/Z+OSRaUsmLtPEYqUxcC1oRqRffxMU7pLKxRvp5enYB7sZA91GPbCie0 bW8ZqhZ4fAo41gBt2o9uOKbpJheJgIZiY6cUk0+MIUvo2D/2i6xWkVHfrtoVkzHj+4bJ anoroZjrO56P1yVsO9F5PsUAKVQXubyteLvbi4usAoLccVBuyZ1Eq56AK+DJ3bT4vQrQ zw/Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b="g/EGpEz8"; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42f 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-x42f.google.com (mail-wr1-x42f.google.com. [2a00:1450:4864:20::42f]) by gmr-mx.google.com with ESMTPS id bp4-20020a5d5a84000000b0030fc90e8f93si266468wrb.2.2023.07.07.14.04.21 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 07 Jul 2023 14:04:21 -0700 (PDT) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42f as permitted sender) client-ip=2a00:1450:4864:20::42f; Received: by mail-wr1-x42f.google.com with SMTP id ffacd0b85a97d-313f3a6db22so2428716f8f.3 for ; Fri, 07 Jul 2023 14:04:21 -0700 (PDT) X-Received: by 2002:adf:fe43:0:b0:314:2ea7:af4a with SMTP id m3-20020adffe43000000b003142ea7af4amr5021237wrs.13.1688763860522; Fri, 07 Jul 2023 14:04:20 -0700 (PDT) Received: from ?IPV6:2001:861:3cc0:bc20:18be:34b6:6303:4da2? ([2001:861:3cc0:bc20:18be:34b6:6303:4da2]) by smtp.gmail.com with ESMTPSA id h16-20020adff190000000b003144b95e1ecsm5285191wro.93.2023.07.07.14.04.18 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 07 Jul 2023 14:04:20 -0700 (PDT) Message-ID: <5255bd6d-8b20-a4e5-bc6b-4f8418bc6700@gmail.com> Date: Fri, 7 Jul 2023 23:04:14 +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 Content-Language: en-US To: homotopytypetheory@googlegroups.com From: Kristina Sojakova Subject: [HoTT] Syllepsis for syllepsis 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="g/EGpEz8"; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42f 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 all, I proved the higher-dimensional version of syllepsis at https://github.com/kristinas/HoTT/blob/syllepsis2/theories/Homotopy/syllepsis if it is of interest. I'll be happy to answer any questions. Best, 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/5255bd6d-8b20-a4e5-bc6b-4f8418bc6700%40gmail.com.