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-ua1-x93e.google.com (mail-ua1-x93e.google.com [2607:f8b0:4864:20::93e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 9f4afc9c for ; Fri, 28 Feb 2020 18:34:11 +0000 (UTC) Received: by mail-ua1-x93e.google.com with SMTP id i24sf350065ual.11 for ; Fri, 28 Feb 2020 10:34:11 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1582914851; cv=pass; d=google.com; s=arc-20160816; b=eHMsCVt++uHzB14wpQA38WHd4WKmhtVTExmrju01OexBAigAY5ltA+tbEY37J2/i9X +x1zNye0IRtsGnFTruZCo2Sj0uMQNqT0ITi9B6rNBlgPZMOcC2XIoCps8GTiqtZ+Ib5a Pzy4GqcISqqTeKZJKJxUjH5fJ2f0DymZI689Earlbz01ztDaR9u+SDgY3ra2FvKtxt8S AkXeEzeusjI89cB7uwYVyHQJJaPhb0Acqcz5LCGyXIex883ugTnQCG13AKIoC7ADKR0q CLHHjR9sdngB+R+f/NIiL7zyg9UqeLj/JNuM0Hbaz5YAp1mRjyIhp2xdQ5FrGMD+A/dq RKWg== 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 :mime-version:sender:dkim-signature:dkim-signature; bh=ddFGfNINoZlpVLjZy8fjXdGuH7OBepIAuRvFO8ibGvM=; b=PyJxtP4+NkczTua0oAG+zZQOW5uklj0l8NUbDtOgfHh+eBkIdkETK/egy1hkkDYjVv 9kpYacR2buvR2X5JgeZTYSTHhoJxM863DrSqSyu5iRjhdwblRuuYs0RaGJ5+2rTzjzye egt15L6NPjZ5WuXkRySBP/yAYnZWsQZu2vSMnH5wSn3rDPCe7ZWN6w2Ak3FjNV7hHPWV AvU3c28FLYrV7250o6lJai+H96PM2DLJW9dDw5wo8jnIQP/DlfqJfAqouhB2KQX3Lyfz TlixYMM87WDqgovnsv43l6hT0r2SVMFh69tPNLCgtD1JIYDID1blwkmHnaDWOCfOb3CQ bycQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=j+NMI6vG; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 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: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=ddFGfNINoZlpVLjZy8fjXdGuH7OBepIAuRvFO8ibGvM=; b=SM4nk4asZsct0pibYtbkLlSGr9ykVuXfz0ZzDpCqSP6oTUUeZydoZFoPPzaLlME/SZ Qpwn4al1kvA/i4TsvJ762uALPAwMnSWQ1nej+qU7d+GnzjDe8j18M6QWYJiDbS5NeP7S 2PstKDmvOEsl5F3vixvSlzqfFKc9W9iXjJ5gP3TSkSmqpQpIAJ40nAs8tAHLhMgvmo1g i7R+bbaFlv5f21ZtSysyNPXaDEKehYFIGJBatsXNExsTvPQvPBfKGI7rUKtWaFYPsxHO vqU3gLCtk1K11QkqeQc+IwPurRgvVptfv8RXOurqdZaXUGN8QOWRAo7h0r5JaxVgJBuq mEYw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version: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=ddFGfNINoZlpVLjZy8fjXdGuH7OBepIAuRvFO8ibGvM=; b=PQF0T8B1IcHdoJrtLbjVOg2RRrXyuM25MX0JjDEQ7hhmiHr16pPc+5cfn80UmaDFjI oW4Or1/9yl4wJGpRxKmecNJBWuiVSNQ5d0IX+NwphRVklxob6tKgkFDWeVud9mPBZG7F cO+e9MDG2RLxnxl2NAZGbjv8st1ZT5H/MX+06L90il3RfyQCgM9Z6FAjcWj0J+rYQECQ 4GcUfoNFnlxdYflHQ6dZmuQ4OetfenMKgw7gGj+DG/WJk5FQQaR7NL7/gfJdzdBkAoLn 32e5eR/kgmuXIiPvymq7deD0REWkkVLJ3H2N1CVKDtYnhbTMpxj9w1QwjwAdIliep6FI dOBw== 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: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=ddFGfNINoZlpVLjZy8fjXdGuH7OBepIAuRvFO8ibGvM=; b=OQTj6+ifgUaM0kyE7rGQLuzLC18hqWwThvMNTayYr8kGmhF/QNkfIDAk2aR1GTstmu gCRfG9m7b55pb954SGOnpqISrHUSBr5lWjjF8plmGNXBViBOSp9dhHN/xNPioxZx6vRu RVSynPaV1E0dVMg7gD2z+mU8jJ7dUpcsGcrQDND3Y68LF8MHpcBKZ421QAuwERJiK8Xg vwaS5g/poGBAgF+HFrwkUVlbhlAQOz6nTOyXrgL/qOZr9mSv1v8gQKGZXvNTgKGI4U/R w+csdGBZweYBrVJXx74m2S/CG9GpA61SnhHJwR8giFaC1q9HAgZPXHv1JCArGNjX4Ekh h3NQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANhLgQ1PyETiwUzAwcjBvp+psicT3qUgu5F7q9nPmWX25zNL1RzZN44R RSeJW2S8xbl0gPm1L/XAVZE= X-Google-Smtp-Source: ADFU+vuhbxAbxR3foqhCA4LL/wsmXNNIn35Or/QyqbwVXBOiWbe3633jEb1gktUr3IkI30m9T7TVxw== X-Received: by 2002:a67:d703:: with SMTP id p3mr3694329vsj.185.1582914850839; Fri, 28 Feb 2020 10:34:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:20a9:: with SMTP id y9ls277313ual.9.gmail; Fri, 28 Feb 2020 10:34:10 -0800 (PST) X-Received: by 2002:ab0:136e:: with SMTP id h43mr2797989uae.90.1582914850292; Fri, 28 Feb 2020 10:34:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1582914850; cv=none; d=google.com; s=arc-20160816; b=o0ceWkh0LrACOFu9Ss3PTd/mgDvxPipMC6mg9YZsBj2qR2ZPS0JOLaNG1J3fNDEZiY ycbwD6xCxHCwnpQqbwZwT+5vVaOWa8o5KaAnzC9tAP0lP74fLzAGthLIrEintuNly8D7 VFZKDkqp8wBwxnXg6wsa6LiSSy5uNjeR7fhqNYb9OdcEQb2S5WcIkhOFoCvDW5HCs5yi prxD66Z+lz1CWsWTkvHZdnMgdWJVqq27ytIJpyzHjBVH6wdeYNvHpBGlfYYSSuE+beG1 9qB/pmHoQt6X5H/yZSLoSSy8Hmgrb123jvHhaw5NXQcawMCDDp3H0Y/miLDxBA31i/3i bNSQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=PgFrKTP1o/Q7J4JiG8Y4OVBX+e8eWW/BBIUgCtP2zCs=; b=coB+McIMh6ePC7edjg6Qr6S5fldQlzyx7iHBeXSem60FwK98pGdlUjlHcN3N8x98GD D0B0oH4NY8/DjKbyI8EPL6iQ16wh5j25Zu6M3Jfaw0ZvRWpSI2RGcMDSPUYrbAQLY51a ExqbNMVLYTsJvd1JrOPKZBDeeNxwsQpWM87PFcnb3ll2pD2MtO91Pw01JcQEjl/uKGb1 0NY8ZFFvw7IFE4ENHarKDWI7VJSor/1UBB0S8zVcS2Uwuy4cCj2VnJQvtCPiOPJHU9HF vhcIXvUTB8gkRu9ng2tpDp27adWs3hafTSBULAbk02weBxINfKGs7sp4vYVatrgfqx0D R9WA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=j+NMI6vG; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 as permitted sender) smtp.mailfrom=nsnyder@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi1-x232.google.com (mail-oi1-x232.google.com. [2607:f8b0:4864:20::232]) by gmr-mx.google.com with ESMTPS id y126si232024vkc.5.2020.02.28.10.34.10 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 28 Feb 2020 10:34:10 -0800 (PST) Received-SPF: pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 as permitted sender) client-ip=2607:f8b0:4864:20::232; Received: by mail-oi1-x232.google.com with SMTP id p125so3762230oif.10 for ; Fri, 28 Feb 2020 10:34:10 -0800 (PST) X-Received: by 2002:aca:52c1:: with SMTP id g184mr4128298oib.154.1582914849410; Fri, 28 Feb 2020 10:34:09 -0800 (PST) MIME-Version: 1.0 From: Noah Snyder Date: Fri, 28 Feb 2020 10:33:58 -0800 Message-ID: Subject: [HoTT] Dependent path composition in ordinary higher category theory To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000004f1591059fa71567" 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=j+NMI6vG; spf=pass (google.com: domain of nsnyder@gmail.com designates 2607:f8b0:4864:20::232 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: , --0000000000004f1591059fa71567 Content-Type: text/plain; charset="UTF-8" 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/CAO0tDg7uSiQrU8%2B0tnwJQHB_AWvRKAxmAePF88GOvd_ra%3DrpwA%40mail.gmail.com. --0000000000004f1591059fa71567 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Section 2.3 of the book introduces "dependent paths&q= uot; (which are paths in a fibration "lying over" a path in the b= ase) and "dependent path composition" which composes such depende= nt 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 i= mportant role.=C2=A0 The problem I'm running into is that I don't k= now what dependent path composition is called in "standard" mathe= matics.=C2=A0 Does anyone know if this has another name in higher category = theory? =C2=A0(Naturally, we'll include a remark mentioning the HoTT wa= y of thinking about this (since it's how I think about it!), but I thin= k that won't be illuminating to most of our target audience.)

<= /div>
The simplest example of what I have in mind here is if C is a cat= egory 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 takin= g 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 example = illustrates that you can talk about "dependent k-morphisms" and t= heir compositions without requiring anything in sight to be a (higher) grou= poid.

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

Best= ,

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:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CAO0tDg7uSiQrU8%2B0tnwJQHB_AW= vRKAxmAePF88GOvd_ra%3DrpwA%40mail.gmail.com.
--0000000000004f1591059fa71567--