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.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qv1-xf37.google.com (mail-qv1-xf37.google.com [2607:f8b0:4864:20::f37]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 20bb061b for ; Mon, 2 Mar 2020 07:03:42 +0000 (UTC) Received: by mail-qv1-xf37.google.com with SMTP id h17sf3478490qvc.18 for ; Sun, 01 Mar 2020 23:03:41 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1583132620; cv=pass; d=google.com; s=arc-20160816; b=zX6QKCnmmujAZCBmPgat0f+tfEeqzDh98JQ1dB+/V6443Wja0EHioqNx1nlsJwTMEC ZVqj8xNJTUipOXE72/OzXHYyFYTLagjFRwUYmytpojxlJfH8PQFuvasdZGcNexd6/yat EgjmkXjPRpSLV/AipMhk563xsAqu9GFS02luSnzh9aq9pOZ7wTwqJZL1AFLd9NyhLcBG kqIDfYfOSqTNp95sK0YMO22U5oirTqI94hmebvjg9lDL89TcIkNBP4c65JChITuZHxTm VJQ7aEuqsY7EpW8KtZ2OTadEej5VjAmiVt0L/fi3RhV1CEeGAbq/gsehTy5VvUIbdw5O lo7Q== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=QWpeGM672Le3iSD3Br8q5V7lZD8bzJOz53RJKSztKNA=; b=CmK2kAATxA5KKXS+3DqDpc6sSV016kNST+8lsaQx2bS63uQQI40eJYGyAreryyzlVt YfMfd++swNCubtamFH+u1XkHwsu/XFkYNH+g0GLV6/gM9fJahp3Y+c5LM+I1at43QDQi kLAxRNGNsZJECWmtrZtP4BLKjfBHtFiaB3bXU3rAymlwNvjUZzvQPFro2uqoJ20xI0N5 8yp2eZzEQysr++p7cp5NH08Sbre7JJZZrAGHtn2TXCuWCnFNcDAVmSmI7AFRUglIiJKG MzTcmwYj11zoNCRcLRD3SRgaGvXuuD6NVUT3xECAFzr2/nBdQh8YdOVniOIxOWq1eyvZ B97w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WenWAwj6; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::235 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=QWpeGM672Le3iSD3Br8q5V7lZD8bzJOz53RJKSztKNA=; b=fJSktnUL9qFJpTWeci2KWTkcBTDD44Q6kJZvSNz3LWaluB4LMlBVxAYZkvol+AjkEv JJys9WmC+x722de91vdIa8JbPw/d9qF8H3C2IBMpax+rNMu9q5IiR5g4TfCoEx/JBoWd pi6I21U6tlzOaZRk16oOA4f1y8GRWp3JJEU8H+jYmwTYO43psknSRxI0GmEuVnmW1NzU rPDHUAfRlSffFYnb7B6ama0G+lzqJabL1JQPUZAlgsbwBChhi6cIBeTjpkBGmjo7G0qB ZS0kbn2h3gohbF9zLPvVjPWtCe5AGQyUmE0Z1uiZQ/2HeYnpbaHUS7zd6gwGaldvirQ0 RnSg== 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:cc:content-transfer-encoding :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=QWpeGM672Le3iSD3Br8q5V7lZD8bzJOz53RJKSztKNA=; b=PC5yciSGzntHYgrpmIx8mzS+w+LXf5KDynG/MzNiXRLGb/L/yxap6Zq8e1YqVxzCrD cYdpu1/r6B8zSiWwxJhqKP5loZan2HrhRf6aZI9OWoweRJPZHIyafe3ZlE2TAkvj+wvL pZSGwCXwYiFLm8lBv3BDNd/2159NutZYzs/i9L8v1HR98Yn2FZMtKouAx9R7YJc7Qslv eJljBgaCCkqmAicKnmqiZj04B/bAZHPcc+6w5bnWMRITurYQbHGQnjkBAK6GVXfoBXsh 2hrlRtiZwRM9f+yPIf54Q2rdXOumhv9SqNZNe8H34nku3F1QZvkVtVvVita8xSuy4VAd Hirg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWURLtSddz34aRKlJCtu1/OOKqZfmiyuOE+NNhMhKXeC9HoVeD6 eQ1zJPq1OMMxJVX9HKJx0H0= X-Google-Smtp-Source: APXvYqxJC6W0WBU5lFN7ASoK/+rHU/TMs0m5I487eAEyDWCUY7li3nfVI1cV5udCa8fB9l7sIAvbVw== X-Received: by 2002:ac8:67d7:: with SMTP id r23mr14430481qtp.20.1583132620344; Sun, 01 Mar 2020 23:03:40 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:7583:: with SMTP id s3ls3964016qtq.7.gmail; Sun, 01 Mar 2020 23:03:40 -0800 (PST) X-Received: by 2002:ac8:460b:: with SMTP id p11mr1728491qtn.233.1583132619990; Sun, 01 Mar 2020 23:03:39 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1583132619; cv=none; d=google.com; s=arc-20160816; b=HOeEfatTXCBSS1h+LB8a1XmzrXwdae8cEiYaF6wFgz0g/L7ZZJt41yuEcUNjzK0/m0 XQZO565Uz4wurBGVwWEAiThARgTQXB1f+beuf2vJ7Wh3xDvJX8htcEE19oraK8ko4sGw sIMISbpR6zccHmVazTae0IVu5b0K4AJqA0Q1sOAGG8cwPFToWf+eIPBgwJWU+CHrZ6O3 yRLB+aICJzRLIdt+14RVZ9FumRcXq+/rBuwPS3BqkhZkY/VoAaib2mUF+WGvFQcR2udV RGk8Y9goMSNyvGbYmy4xLavt4sHk6bZlr2cwCrzoyl6CM98YEe0She7+P89Ih//3Yzd0 idUg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=0ozOZrOC0kR4DKMxslQxnKJr86FMQzVWoEA1nhxeZsA=; b=EwterqOt9A3lLltJDW4jYTKTv5GtsDdm3fXGe8GsATnl7OAN9jsi2Qv1A/Z6q7tmmj 3adXETWuGTlUlDlGlXWOkBSbYdl1msNvzKvYpNNeKehsUYG72FL5yyyAAaZ4eyPbSIhh DfFmojiXzGE1EGmiQTpUsamSdYD9fvF1BQLz1nevpqCa3QRuFbifHdGmukB9leW5K+xl mj1uV14nkDhh3C2/+xRoqohBos69cUdH+HZFQ59LLAUp9WtT4S226T7LCidAuVk96qQ6 eggPaqsLiVNzqJCiR9pGVXENKgVqX1MRzgfN7aT4Auz4kfcMz9gS0WgK9KfaeWk8gpik n2Hg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WenWAwj6; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::235 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-oi1-x235.google.com (mail-oi1-x235.google.com. [2607:f8b0:4864:20::235]) by gmr-mx.google.com with ESMTPS id x18si634340qtk.0.2020.03.01.23.03.39 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 01 Mar 2020 23:03:39 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::235 as permitted sender) client-ip=2607:f8b0:4864:20::235; Received: by mail-oi1-x235.google.com with SMTP id l12so9282978oil.9 for ; Sun, 01 Mar 2020 23:03:39 -0800 (PST) X-Received: by 2002:a05:6808:8ee:: with SMTP id d14mr10033451oic.138.1583132619210; Sun, 01 Mar 2020 23:03:39 -0800 (PST) Received: from mail-oi1-f171.google.com (mail-oi1-f171.google.com. [209.85.167.171]) by smtp.gmail.com with ESMTPSA id k25sm449745otl.34.2020.03.01.23.03.38 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 01 Mar 2020 23:03:38 -0800 (PST) Received: by mail-oi1-f171.google.com with SMTP id r16so9286440oie.6 for ; Sun, 01 Mar 2020 23:03:38 -0800 (PST) X-Received: by 2002:aca:1a06:: with SMTP id a6mr10220384oia.148.1583132617732; Sun, 01 Mar 2020 23:03:37 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Sun, 1 Mar 2020 23:03:26 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Dependent path composition in ordinary higher category theory To: Noah Snyder Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WenWAwj6; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::235 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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: , Yes, I think probably you want indexed categories, incarnated as fibrations. You can then remove the invertibility too: if C is the 1-object category corresponding to the monoid of natural numbers, then an opfibration over C is a category equipped with an endofunctor, an endomorphism over the generating morphism of C is an algebra for that endofunctor, and its n-fold composition with itself is the corresponding algebra for F^n. On Fri, Feb 28, 2020 at 10:44 AM Noah Snyder wrote: > > Mike pointed out that I didn't explain how my example is a special case o= f 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 algebr= a for that endofunctor (where the map is an iso). If you dependent path co= mpose it with itself n times you get a path over loop^n, i.e. an algebra fo= r 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 compositi= on" 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" pl= ays an important role. The problem I'm running into is that I don't know w= hat dependent path composition is called in "standard" mathematics. Does a= nyone know if this has another name in higher category theory? (Naturally,= we'll include a remark mentioning the HoTT way of thinking about this (sin= ce it's how I think about it!), but I think that won't be illuminating to m= ost of our target audience.) >> >> The simplest example of what I have in mind here is if C is a category a= nd 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) categ= ories"? >> >> 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/msgi= d/HomotopyTypeTheory/CAO0tDg5mstbw3Ujjfu%2BkMfgW7_7y7raxbWV_yh-2phB2ynwb8g%= 40mail.gmail.com. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQzAoLQkXUNDkauM5so1rNu9-LsyWRHM4xO16d4O8Wt-0A%40ma= il.gmail.com.