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 31551 invoked from network); 5 Mar 2021 18:40:21 -0000 Received: from mail-il1-x13b.google.com (2607:f8b0:4864:20::13b) by inbox.vuxu.org with ESMTPUTF8; 5 Mar 2021 18:40:21 -0000 Received: by mail-il1-x13b.google.com with SMTP id q3sf2467341ilv.16 for ; Fri, 05 Mar 2021 10:40:21 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614969620; cv=pass; d=google.com; s=arc-20160816; b=t27TKpC4wtyIIUxoDvtvksi4LpppUMpDccDbBjt20lup3oNlvOSxHZZdJf8TDQkOgs NzGL92MzTWretiQMQPp/GtIjiaQNnNcNBIIJOIkoz0xsJQ2DE4P58gkhaIX2/0CmhnlU qDvaCzayK4RYsGbQVJ0LOrinD/pIw5oywMyzlkUgEl326rXuYSNcBnJ+AF0A7GkqWei2 1SIGJrsdbcrgDrZIUGUnhS8WKGoqh7Y5T3itvcLZ4oeD33ku3CzHNPFpzOfNiUs8qqKw QxzPcBQdxqB+MBAbFX9me+vFj5EQMHOXrUv0v0kRZ6H2jbq6HHyYhRdkoMGIaHpHArOd CM4A== 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:cc:to:subject:message-id:date:from:reply-to :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=38kzjZctldNIsDin1Blfslmv1Qk1Mu9Dc6Ipqq4P5Jg=; b=QwuEloEw2kaKx87zVR0Hz5X0IzO1yWS5eZczEXX1gHmo3pbKTs7/OBDQ+LnsZgxjps aloxwHlHXawIaWsA+h3Pi1/G2ZJty5JhGr4a7oDbm+38F5Ofe84syadc+PlTj4gyA9Tm Db7CH9Rbr5GDJoFxDg0u7cX4fDafT1hQ0Lf9DoviK9016WaWD0lPjKRU14UZ0ktccBrd vVPDoNcXkeKEFa18yfVa2hKpZboW3wuJIlD7rvP6Wv9SZLjawi7CjsWCWw7H4WFdWd3L ugd9U3FbPfiOAIXnIwFvqf4lU/+gLvZAnLC+s9oM9oUkYF7p0DxNt2qz1KzO047XNOx0 GcXg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ADf9jCzv; spf=pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d32 as permitted sender) smtp.mailfrom=jamievicary@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:mime-version:references:in-reply-to:reply-to:from:date :message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=38kzjZctldNIsDin1Blfslmv1Qk1Mu9Dc6Ipqq4P5Jg=; b=gC9HXV0x8qMZiZfXW48bz31tg4HnEI+1sZRDUrP1BUcsoKRoVqEKs/Ty4saY+3yYo5 wF/3anZzlRlTr7FTq82zJGP9XPv2bw1gL5nP+0NT4listD0BB6Yo+5nWU2ESWPR0qO0n l926iMJKgoqzFDO3f6IJI0+geZJzbScnhTLMLbc85oXV2OpTMCL7tDtQ4PhW0MNi2kvD WXmMMGUfRZARk0A0C2gBVHhgbMgj+fHXBbdMBMc9nAK5hgmfKwKYV/2pF9kBKACQD3Us 3xVYZphiyEc3O1vuv58RZkV6Y22JZMqN16f+wVftC/OfQBXwXqJ0IqEQ/ca5qxCskv/j UlDw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=38kzjZctldNIsDin1Blfslmv1Qk1Mu9Dc6Ipqq4P5Jg=; b=N6eJsP+aUupZg2I5LPF8HCLxjg6AtTG2oGGzlEI16ysh8CXRXbBK/1hM+qz5pcw+XO q621pOi4Hu6vIyvTx40lgwhoxtILjymiv95UTrmVQ11Gshn3F814fyUG7lXaIgC2fKMR 5qCZJthePjX33lJnF7zdeiWYX7DxLwufzJHepKi1i7SjjY/RXI4jPQMamChWmzazYbyX ZFaARYJsAuqg0tiv6NxWyYPSR0RVkLUfNgrDvfP3h4lciiAwvoOgduskGChshX89n1Gq qXLg+TcK7k7voyp3z0WJTZ1qHBWWscicGP/t953b/NfI9pPH+PkWKJhe1ucJpQykSlV+ DpRQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to :reply-to:from:date:message-id:subject:to:cc: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=38kzjZctldNIsDin1Blfslmv1Qk1Mu9Dc6Ipqq4P5Jg=; b=YVddj6uUWejfR/JlBo/NL6JPPzNjfsD+R6gk3FKyCPinljuVfuWdNFi2ggYswjeao/ DvEArDbJr9SixvfiC5E3t+F7nop/9l4591i4f3UGNOHK5YbLl+KVWJCokr52chrcAwcY Fi6AHWOPkJO0zBZJk5PeuzZhEOBBH0y3z9U7HJ9CMgbEHcx3EKXQBFobou1XDUFN5Qbs N516zzt/+tdxz7UvnlG/gmPAtiGTXiL6dFCWp4JeTWLu+TGDPkluBWwegreVqDOKv3HK XcpwYt7zv98TKiBDKfN4tTOSUR07KDFE99iOsITJUof3hzVnxInmy9d0BxZ3/8/ZSD89 BWkw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533Jy3nyMUctAAsMQoLgm9xSAm5kNd9pOMP4IIskIzaxI9ka6Y2p i3QeSPJ2VfUMHKPwRU082us= X-Google-Smtp-Source: ABdhPJwxsKuk7wQYxkThF6ZuE1Fx5uS7UCRLIpzoTvLi85Q2A1Ifqk9ix0t3W7Ypq97BIN1QvL/8PA== X-Received: by 2002:a5e:cb4b:: with SMTP id h11mr9622533iok.108.1614969620076; Fri, 05 Mar 2021 10:40:20 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6e02:2195:: with SMTP id j21ls2705462ila.4.gmail; Fri, 05 Mar 2021 10:40:19 -0800 (PST) X-Received: by 2002:a05:6e02:12e3:: with SMTP id l3mr10184600iln.24.1614969619720; Fri, 05 Mar 2021 10:40:19 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614969619; cv=none; d=google.com; s=arc-20160816; b=u9Lyrd5q+QO6E3mf3r9KBAStWl8cBQlf8lf1BBubn7GVhCdC+hh0r8AC7tzCOraQMr FuqiVM+23h+ZYQojWLYcRRd+M8qIrwM8WAawzQEu0JHgZrX7j9XltDzbFRD6jaIk/TT3 u3hv9Sxl3gQKqPbQKRCgfOj450zE8qo1C0YF7//Dc1/aknoytu1ZoH8aStJQsBDkUVVY SPYsqIMYqVwaZmddbuf5V7TWXsyarHZKqhuV4h1h2QcXUdbGSqCNbr1p2ZGfgzvblraF OtlmlbMNQHwQeUe1RienRQS1/wquzxOBogOA5VaZOoC+V7pfltkrOs7SYBBAGPNavFxv J9dQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:reply-to:in-reply-to:references :mime-version:dkim-signature; bh=4ma2VQcEHrA3E3qStUB7rXtKA4VPTsuyDQPILGb5GOk=; b=DLlV0xASVb/RfADt1Api+vtVay5H3jehg62th7Z2ZeKuhApMIyiW5wknowHVtABvC7 dwqweiLyvuICZaam5Ccbx002bv9KHGTnxTbsMWs+ueqcNC4RRE0MyP59OxfoA1KkvD1p /Ms7wrbHdZ7EYvdxJGs7fxJRRog8sq/NdUotErdQZ1g2HsSx+ZQVFpk8EC+T/T/nFs3q H876q7tqbi9SmxCW/k97/xmk35zesm2cyuOIcL1n2HkOZ5d1aqm6nFobguOVCCBVVFMj AA08kVXsEFsfnKhCG9V2bheagOdjR9Y1C2LH2v7r9Wq2pYQEbDPNNeHjUiM9XEVQhn1H FlAQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ADf9jCzv; spf=pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d32 as permitted sender) smtp.mailfrom=jamievicary@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io1-xd32.google.com (mail-io1-xd32.google.com. [2607:f8b0:4864:20::d32]) by gmr-mx.google.com with ESMTPS id c2si265753ilj.4.2021.03.05.10.40.19 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 05 Mar 2021 10:40:19 -0800 (PST) Received-SPF: pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d32 as permitted sender) client-ip=2607:f8b0:4864:20::d32; Received: by mail-io1-xd32.google.com with SMTP id z13so3042468iox.8 for ; Fri, 05 Mar 2021 10:40:19 -0800 (PST) X-Received: by 2002:a5d:8249:: with SMTP id n9mr9502522ioo.31.1614969619365; Fri, 05 Mar 2021 10:40:19 -0800 (PST) MIME-Version: 1.0 References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> In-Reply-To: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> Reply-To: jamievicary@gmail.com From: Jamie Vicary Date: Fri, 5 Mar 2021 18:40:04 +0000 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Kristina Sojakova Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: jamievicary@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ADf9jCzv; spf=pass (google.com: domain of jamievicary@gmail.com designates 2607:f8b0:4864:20::d32 as permitted sender) smtp.mailfrom=jamievicary@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: , Hi Kristina, that's great. I don't know that anyone's done this before. > Given two higher paths p, q : 1_x = 1_x I guess you mean p,q:1_(1_x) = 1_(1_x) ? Best wishes, Jamie -- 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/CANr23v3E%2BkaPKgL-So_s_h95KUwSM5i1vPSqzQyEmKa%3D_D46iQ%40mail.gmail.com.