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,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 4631 invoked from network); 8 Jul 2023 12:22:20 -0000 Received: from mail-pg1-x540.google.com (2607:f8b0:4864:20::540) by inbox.vuxu.org with ESMTPUTF8; 8 Jul 2023 12:22:20 -0000 Received: by mail-pg1-x540.google.com with SMTP id 41be03b00d2f7-55c072efe78sf2658951a12.3 for ; Sat, 08 Jul 2023 05:22:20 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1688818939; cv=pass; d=google.com; s=arc-20160816; b=pUXK7NUiEsNdgf+zpt+fkKRyOvUKTukxlVNoDqL0lhwPcAeocQuWds5qwEkV2TetI/ f7O9xRPwsUwqzb2u3jKqtoV+BDhfRXmQwuTxPUZZL8P9xW335m0wGEur+xCiLQ8H/I4x SK0AUXTzmKen0bdA4Y/ecW4qlHxH59IQxT29xQASlhfWvqCSJpKpE44h/ligtGWPHymc SMsnJxsOKMrHRU+P5lUMfV5e3Df8EzsYixSUOakO8FyscMNkLQu0+UFkjXrBx2J20+nT pYMjmWzXEpt5Cs52mB9eQdPcNl5MDUfD1aZBXbwJK7Vmi1YMJqqVZyKi1eM4q+9ilQUI IhMg== 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:message-id:in-reply-to:to :references:date:subject:mime-version:from:sender:dkim-signature; bh=mvynviryr18q3EUEMefwsEAwqEhHuHcdVUPbrqitZAw=; fh=7q7rWnV/hiRmpF1dRMfMF/snm45drpQQlt5AYsUIAPM=; b=wfWJl2wJAtOJEMZ+kuhkIIZPlKkneQ2JevT19lDFE13n8396J/ZE4XZnJ5Bm1rkIho ATyZbcdbF7JphrruIkrO/bYNwO4gbBd5T1dzIabvIXdA4dFZts05t82xdxCBWKzkcnsx fg0KkJWL+CbjFWja3nrRMMINgHnoTUxQmeksnY4eumN6rSohmRyD3tTs7fHdA/3maZQ9 L5+/PuOjk/mOd6xpw6bm2hd98K3kC4gePVuqKN7jD1enzZ6btP6ThEJKEWYMUCrGbahH RxiDvwpcIxFwe1xGF2QqBz7LfjowNi9Ms6/oqGw8u5+vZO7a+UbjCFkK7LUOoFnGBOeN 4D8w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=SItRduYC; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.10 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1688818939; x=1691410939; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:message-id:in-reply-to:to:references:date:subject :mime-version:from:sender:from:to:cc:subject:date:message-id :reply-to; bh=mvynviryr18q3EUEMefwsEAwqEhHuHcdVUPbrqitZAw=; b=iPTF/bwwsqcnMAX1u6OoLmIh7df1VcQUtDjmfSjkRDnKZUIJw8xiEfzVRuBd6pV0V9 RPCZW8/moaecAii4UXnAecJsYXtl+zCqch6b2BORdTtXHcIb5cxETCc0QB7R7LefLvlp mE8fKXj8ezz2l+Bxr/zogWxO6imbe1UQqjfRaZ1vsYr5fjOGMIGqupMGI/ADFGoQRoGm BlVu2PiUGU39l5HLJTp2GCPR9b6gKSirPRUwK0Rzd1aEmqs4LKbp8NRCKGDwAd3EKEuF 8pGmeXZVUj0ifnzZKGwgvJ9x0PsnyeV5d+jBcKAu/gEPWjxRTbSvXfD3wx0NdhB9Vyrn VLQg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1688818939; x=1691410939; 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:message-id :in-reply-to:to:references:date:subject:mime-version:from :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=mvynviryr18q3EUEMefwsEAwqEhHuHcdVUPbrqitZAw=; b=beXMh5dadFx0e4TClDc5bu3q9leflxdy3KzCWxdoqwAJX8+YybkBrH5elQ4fVv5Sr5 rWRpxu7xn/Vmp2MdBxZS65iIpYJ4UiNzbzFrjKrBPNoigsuLRWP4rleCudCMbbFnWBr4 istGz0OJBp6KRiOWQATdRUd+yUKxx6XHWyaHhEdFeEO+2ZYzuGO9o2U+FwITAWWjpd35 nrHmA86YN6+/CwK/bjbt5yxLd898Gu7fVxI3X3dT4ghLAdLmCS8ch5BrvwVW2aaVJLoh yphPJEEkmqyZtksY0g/WOqdbO/hEgWKblAu91nZ6CiO+RrBDpeCI5fyZjU5O0EIqf3gb BRRg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLb/9i+i48oW+tJ5QcqJyc1mJ4UH/yley8K/4uhBeudMVMbKM+gY nZLAtgzvyhUw3aFBRkTWJcM= X-Google-Smtp-Source: APBJJlFz478kRbcctLj4GutCpZIQgUTPdtjhHZqDIye5DMu0RAJYjpYZFc43CoHCha+8s7Q38S6U2g== X-Received: by 2002:a17:902:da92:b0:1b1:9218:6bf9 with SMTP id j18-20020a170902da9200b001b192186bf9mr6877920plx.43.1688818938897; Sat, 08 Jul 2023 05:22:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:903:2886:b0:1b8:9fc4:26a5 with SMTP id ku6-20020a170903288600b001b89fc426a5ls1328296plb.2.-pod-prod-01-us; Sat, 08 Jul 2023 05:22:17 -0700 (PDT) X-Received: by 2002:a17:902:b418:b0:1b8:1e05:ed09 with SMTP id x24-20020a170902b41800b001b81e05ed09mr5228080plr.36.1688818937111; Sat, 08 Jul 2023 05:22:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1688818937; cv=none; d=google.com; s=arc-20160816; b=DTKhDx89RezB0Gw2tVBt0YHZesypXYVuKC2wBgZlNCx5htWMLvDtAFXzqXd/OEn5Fl yG8uqrEESAChjnfAxcYBWB0r4kgZ2DQaDSSSurnsKLkNSBgFF2Cd/TVeC7k+RYosqjc1 k9yV+9UVlzDw/rpAUZb2Yw3ysTDe1l7D5B8Fi+er3OFIzAJVWc6jjjnG5KJtPUTbvVmR wjfUmJNfUYr4rF7FGUNPlp34xHrmAFVw36QfyeL8ICIvf2RPDurau33KY1QyIQSfy5L2 uJXY4tlk+oodFlemElh4lvJ7mepwaw5w1QCkKk1MUqU0optk1ZU2NjIskFESNLMEFmql Oe3A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=message-id:in-reply-to:to:references:date:subject:mime-version :content-transfer-encoding:from:dkim-signature; bh=RD4RToljON/h5/raBplOjT6QFvOovNLef/LgtliY6Y0=; fh=7q7rWnV/hiRmpF1dRMfMF/snm45drpQQlt5AYsUIAPM=; b=S5AdP8KpdvVWrgVcrMGqT7+gWrf/mZIi3uLZGXDBUWAjtNNAzKqg7TFZOm9kmf2aM0 BvLmf70qHXXRu8kH+5q34t62hU2z3t2FDqdXYXNECorsrTE2v5sviZXupneDpgfOYm9J nn8vKpDmydQ+jhQRdo77UvV7NRQ66wfoo1Fd/FqXN0Y4mPPBrmC24cos+5re8RdfjxWp ivG00K3rw1N/4342KtnT2hTCLYFxVzT16QLQP4URn+LkEEUotoFp94/C9bYEGk4vVbdB zli65BKOdle9ic9k/TtmdEXLyRf0YpY90neY+sNq9s4/4Ms+II2Q9IQY8JPChv0dMA1X RVSA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=SItRduYC; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.10 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.com Received: from qs51p00im-qukt01072101.me.com (qs51p00im-qukt01072101.me.com. [17.57.155.10]) by gmr-mx.google.com with ESMTPS id b2-20020a170902d88200b001b878f9e121si290904plz.0.2023.07.08.05.22.17 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 08 Jul 2023 05:22:17 -0700 (PDT) Received-SPF: pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.10 as permitted sender) client-ip=17.57.155.10; Received: from smtpclient.apple (qs51p00im-dlb-asmtp-mailmevip.me.com [17.57.155.28]) by qs51p00im-qukt01072101.me.com (Postfix) with ESMTPSA id B007F401D6 for ; Sat, 8 Jul 2023 12:22:15 +0000 (UTC) From: andrej.bauer@andrej.com Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.500.231\)) Subject: Re: [HoTT] Syllepsis for syllepsis Date: Sat, 8 Jul 2023 14:22:04 +0200 References: <5255bd6d-8b20-a4e5-bc6b-4f8418bc6700@gmail.com> To: homotopytypetheory@googlegroups.com In-Reply-To: <5255bd6d-8b20-a4e5-bc6b-4f8418bc6700@gmail.com> Message-Id: <1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56@andrej.com> X-Mailer: Apple Mail (2.3731.500.231) X-Proofpoint-GUID: OUis_BqjRs_1rq55HIrqaqh-l-PNnCjY X-Proofpoint-ORIG-GUID: OUis_BqjRs_1rq55HIrqaqh-l-PNnCjY X-Proofpoint-Virus-Version: =?UTF-8?Q?vendor=3Dfsecure_engine=3D1.1.170-22c6f66c430a71ce266a39bfe25bc?= =?UTF-8?Q?2903e8d5c8f:6.0.425,18.0.572,17.11.62.513.0000000_definitions?= =?UTF-8?Q?=3D2022-01-11=5F01:2022-01-11=5F01,2020-02-14=5F11,2021-12-02?= =?UTF-8?Q?=5F01_signatures=3D0?= X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 mlxscore=0 spamscore=0 mlxlogscore=617 malwarescore=0 adultscore=0 clxscore=1030 bulkscore=0 suspectscore=0 phishscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2212070000 definitions=main-2307080113 X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=SItRduYC; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.10 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.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 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/1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56%40andrej.com.