From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pl1-x63e.google.com (mail-pl1-x63e.google.com [2607:f8b0:4864:20::63e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 277f11b1 for ; Fri, 28 Feb 2020 18:44:32 +0000 (UTC) Received: by mail-pl1-x63e.google.com with SMTP id m9sf2205075plt.13 for ; Fri, 28 Feb 2020 10:44:31 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1582915470; cv=pass; d=google.com; s=arc-20160816; b=x/aWQuIFjW5uVCxVd1c3wMm2MHAKN5TXBt4HGO2w2HDomeyN3TRFP1Ej2LLtWciVav CtU+oyAa0Hd/F9T3RfQCHw25e0TEszASw8+ltSFoQ02XVehGWUwQzCcB3Eou4SuLqj5T ycRmpEbpylojYzzp50v2l6L2i/fGj7P1f+ti5mTG5n8b9uXH9ch7Xu2ulo53zz7giwhh PRcY0kiQUL6LAe3AAUfFz9A8qs0j9FaTDIYM/22AI+o0Ew2gLED1CD5fsOd3oRNE2+yq yRWahFnKgRgw1XVM3J7G5/cco9hNUDDOzM/ade93x8HSdd7jdYCF9cf4d7CSGCNnTXlg ciiw== 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:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=hQxgm964pN3V+ZbSTiFEKOaxZJsbjPM2Q156+/GSqw4=; b=GYa908rPF/zy8gp5aOWZyLQoQHRJ9Hm29pA+OPjDtR9Y4dQXXZYE7PK9jZJF4xjO21 leJy3umDOxMmAuQDaXvVpfNKKe88daLNcL1pdpt9R6HWGNrxymHSJoBp9bDPJ/3j1t0s 5bmohpy9UeayAQP2rPnqROtHIYv44xApoL2wBteQnpUhCcUUZBk5NDcBkGxiS72YNFJv olY6QJxma0Y/uwgjyLxJgFOsK8vVl//AgWhm72qOcIDkWI7eMCGxgC9+v+qRt8thW6FN ZkA/7SsU8t9ulSpeVVFDPnHS8G5dJw93PLNTpO3rumMwgtSsTKq87SoBlHrpeSCiWmh1 g71Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="i/sBEErM"; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::22a as permitted sender) smtp.mailfrom=nsnyder@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:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=hQxgm964pN3V+ZbSTiFEKOaxZJsbjPM2Q156+/GSqw4=; b=s9XWSpVd+XMk32ViiYHqBJ2QrGLnzOUwnUTOxx3nJPgy2SFMY7rZgTAtbkSqGWAbwP xz0FtdHxmj0ZYLue/83HI9kJoGn6ikVgpuxjm3Jwl6AftKHMxm2ty8uHnfzQCuFX7J2i c6Duf1VYiYm6Fjs21jyom7G3/oy4xFnFRTDK5/kbf9dtR2vRYl8GpewZtnqmMC2Adv+0 ZzpIpPt9AVaX0vlailsstEncqYNFywIY4t7E6TJ2yZMVQ6it3rYjUfFzeEYWsdPXrC6/ cepvtUk/ZmpWcSlxeRQyyEqhDrEdaa7bAcnagFCmVcOmpHpfK7vLmz2sN4mUhKOXoIKf 7OOw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=hQxgm964pN3V+ZbSTiFEKOaxZJsbjPM2Q156+/GSqw4=; b=lPKErqRUHIZm74htb4BilRHmQu9qrQ7xQUcn/gVUEzXCFlBItxeiFgNNewY+ZINxNe NspJ2k5HIMBeSRBJRCSrPffjjInmfNKz11qoXHoOmeWQ1RTX+Ah16GDOFgudqyhlwB1O DS6hGNgoe0Puk7nl+C9cJqN4kQ70MGm19jenye7qTEQGBvQXA8uKgX2ktcXRaJs2X0U6 HVVemgxiMFtgYU60U+0LdqCo9mYbqVOT8XcuEx393TKPFNF+VyzlbimSLq1afvgLGTyW HvxNm5A+pod0tmVpJPZR3OJthz6EVzgy7mS8Ef4TC2QLnl1NfQJzewcKymBZurqOxFei pi0A== 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:from :date:message-id:subject:to: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=hQxgm964pN3V+ZbSTiFEKOaxZJsbjPM2Q156+/GSqw4=; b=uNHqjtGD6L+UElyxSqGJvkZ+7ALaSrBAlmv9hlB3gt/qXs0pUgTnNAFEUSc6nFm2+N 7uwM+2an3MNOC0XSjrYz4hFRA7pqsq3Lf0DCk7DxEMpI2RKevLdLkTmvQyUUGui1FnXC qJRoDMsqihKNfD4AkNdf09aZdP4nrW9P8RJra72ng4KuzZ/O+kUZ6B9vbn5nD+T9PCuD MrM9vydmGnej3lY4Gn96xv5YwXTF4qa878JTPjWNAcajclGzXQJowZ3la0PH0Z2DQiII fABrl5Orv+/CbKxQvENpMYbyKXVyJpUQ0TcaUnJBp3tFpRgP9b1V4X8IYXjdu7zinQor 3X3Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUe8zYlIDBITYSdKI1FCXTgVOyCn7MrFlJKpNzXnVAp0lWpMjLi 15uYvgcLVmLeOuaHWSrZKuI= X-Google-Smtp-Source: APXvYqzsU68smvjDlp+XveCdXuwCdOEyxzIYh+Yn1CTTBhjQv6MgOnmg7aRGGB6u8lk9yDV+FLUkgQ== X-Received: by 2002:a62:5547:: with SMTP id j68mr5940950pfb.6.1582915470460; Fri, 28 Feb 2020 10:44:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:e795:: with SMTP id iz21ls1245068pjb.2.gmail; Fri, 28 Feb 2020 10:44:30 -0800 (PST) X-Received: by 2002:a17:902:be04:: with SMTP id r4mr5220636pls.315.1582915469983; Fri, 28 Feb 2020 10:44:29 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1582915469; cv=none; d=google.com; s=arc-20160816; b=evKo3PoxbDBwavpXwsnYWsjCK1zw45DrLWshnb+oW8WFX6mB40SrcVOeuAlATYj91R 0Xbh/+d/owrvEWJvElzRX6QX4B9Me+Rwz2E3AwQJxxtUPVetqp0AFAtNYmmaRZhsTz9x Upq7GYLkf342PZcVMqC3r4go9PIFVozzYnhwyhZq/TFWUslxx1SnjWbAX7zLiLgM9HPr +jKqO5Z9Qjtipy7ersSOeCrRhMYBHZHRbO/hiieQtLx+EZZYDUWiLWP88fP7gfFY7HkA Namwu/X53OuSu7/35zz+Kv866X6CXpAOt7+eSNrpBPKUX18fd5Zr802i6dx1zE//4tDo QUqw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=M/7qTXFl8f2Z+h1gsaqHyuhPBnVhD+RJaThUjiggFHE=; b=p3XNw84GL9Smcxwb622gXveTFMcEsnnP6tuAHmofJv9n2tOCOY3+h0zuRLKs5V/5I9 qGv00MksBhvxe2htzSvbDpiBulmfyI/vd2GMDwQ7dlVCc7dfSUTSzbgyY51fj6wcbe1L CWVS2xSldic7JdPWmSVVVHuSFjWfmwy8iO++7HrExhbHMmrSwAyK4HOCoyrt6OzXSa6X BZQ3PKunxQpP4rLLit4nCanj86BPaf9AI2yryx+rwHycz+Xl3NH728lNj3zDLd6klQff mROFisoV4K1OM2A68Xh9iz1AtyKvSt575cjNgzAWz0Er18V7dyNX/yOMGjhIm7KYNHbJ eE6w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="i/sBEErM"; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::22a as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi1-x22a.google.com (mail-oi1-x22a.google.com. [2607:f8b0:4864:20::22a]) by gmr-mx.google.com with ESMTPS id s92si85315pjb.0.2020.02.28.10.44.29 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 28 Feb 2020 10:44:29 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::22a as permitted sender) client-ip=2607:f8b0:4864:20::22a; Received: by mail-oi1-x22a.google.com with SMTP id l12so3797893oil.9 for ; Fri, 28 Feb 2020 10:44:29 -0800 (PST) X-Received: by 2002:aca:52c1:: with SMTP id g184mr4152172oib.154.1582915469336; Fri, 28 Feb 2020 10:44:29 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Noah Snyder Date: Fri, 28 Feb 2020 10:44:18 -0800 Message-ID: Subject: [HoTT] Re: Dependent path composition in ordinary higher category theory To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000426621059fa73aee" X-Original-Sender: nsnyder@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="i/sBEErM"; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::22a as permitted sender) smtp.mailfrom=nsnyder@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: , --000000000000426621059fa73aee Content-Type: text/plain; charset="UTF-8" Mike pointed out that I didn't explain how my example is a special case of dependent path composition. A type family over S^1 is a higher groupoid together with an (invertible) endofunctor F. A path over loop is an algebra for that endofunctor (where the map is an iso). If you dependent path compose it with itself n times you get a path over loop^n, i.e. an algebra for F^n. Best, Noah On Fri, Feb 28, 2020 at 10:33 AM Noah Snyder wrote: > Section 2.3 of the book introduces "dependent paths" (which are paths in a > fibration "lying over" a path in the base) and "dependent path composition" > which composes such dependent paths when that makes sense. I'm working on > a paper that's not about HoTT but where "dependent path composition" plays > an important role. The problem I'm running into is that I don't know what > dependent path composition is called in "standard" mathematics. Does > anyone know if this has another name in higher category theory? > (Naturally, we'll include a remark mentioning the HoTT way of thinking > about this (since it's how I think about it!), but I think that won't be > illuminating to most of our target audience.) > > The simplest example of what I have in mind here is if C is a category and > F is an endofunctor and c is an F-algebra (i.e. we have endowed c with a > chosen map f: F(c) --> c) then c is also an F^n-algebra by taking the "nth > power of f" which actually means f \circ F(f) \circ F^2(f) \circ ... \circ > F^{n-1}(f). In particular, I think this example illustrates that you can > talk about "dependent k-morphisms" and their compositions without requiring > anything in sight to be a (higher) groupoid. > > My best guess is that the right setting might be "indexed (higher) > categories"? > > Best, > > Noah > -- 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/CAO0tDg5mstbw3Ujjfu%2BkMfgW7_7y7raxbWV_yh-2phB2ynwb8g%40mail.gmail.com. --000000000000426621059fa73aee Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Mike pointed out that I didn't explain how my example = is a special case of dependent path composition.=C2=A0 A type family over S= ^1 is a higher groupoid together with an (invertible) endofunctor F.=C2=A0 = A path over loop is an algebra for that endofunctor (where the map is an is= o).=C2=A0 If you dependent path compose it with itself n times you get a pa= th over loop^n, i.e. an algebra for F^n.=C2=A0 Best,

Noa= h

On Fri, Feb 28, 2020 at 10:33 AM Noah Snyder <nsnyder@gmail.com> wrote:
Section 2.3 of the book introduces "dependent paths= " (which are paths in a fibration "lying over" a path in the= base) and "dependent path composition" which composes such depen= dent paths when that makes sense.=C2=A0 I'm working on a paper that'= ;s not about HoTT but where "dependent path composition" plays an= important role.=C2=A0 The problem I'm running into is that I don't= know what dependent path composition is called in "standard" mat= hematics.=C2=A0 Does anyone know if this has another name in higher categor= y theory? =C2=A0(Naturally, we'll include a remark mentioning the HoTT = way of thinking about this (since it's how I think about it!), but I th= ink that won't be illuminating to most of our target audience.)
The simplest example of what I have in mind here is if C is a c= ategory and F is an endofunctor and c is an F-algebra (i.e. we have endowed= c with a chosen map f: F(c) --> c) then c is also an F^n-algebra by tak= ing the "nth power of f" which actually means f \circ F(f) \circ = F^2(f) \circ ... \circ F^{n-1}(f).=C2=A0 In particular, I think this exampl= e illustrates that you can talk about "dependent k-morphisms" and= their compositions without requiring anything in sight to be a (higher) gr= oupoid.

My best guess is that the right setting mi= ght be "indexed (higher) categories"?

Be= st,

Noah

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg5mstbw3Ujjfu%2BkMfgW7_7y= 7raxbWV_yh-2phB2ynwb8g%40mail.gmail.com.
--000000000000426621059fa73aee--