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,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x73b.google.com (mail-qk1-x73b.google.com [IPv6:2607:f8b0:4864:20::73b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id fcaf31ea for ; Wed, 7 Nov 2018 20:00:28 +0000 (UTC) Received: by mail-qk1-x73b.google.com with SMTP id m63-v6sf32942891qkb.9 for ; Wed, 07 Nov 2018 12:00:28 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541620827; cv=pass; d=google.com; s=arc-20160816; b=cOsixU6mtaiBAM/9cAARolWzBmVOAL1q8Tmzc7mts5JGZ8jtIh8eU4aZTItROD4ibB FXr0++RQQCHF2UQNWRyjV0xMq619mAOoqf02HJBaOiTfDUjr1Vwa7ujkGeIF8W+aLr1f EkyqTSGKAV0PPpsD0K0xdln05aT5DPCoIrQsD2Jkj6diud0Qow72JuUjwrBB/85lCQvQ Al/zj9Ti4aAuDegSbxIsbfcYYXdNwkcpFrKZSuEOfa9k4vY+guf5R9wRDQBjV+xjK35B 3swr6tXXbHJnXlGsfSKT+hcl0EC6rosKCb7cg72ndSiDsntOxOF2Kd3OS9neKBj4dfp2 R5XQ== 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=4iL5Kiw7jvRWSjj2hWgApO4ExOWFA0BUI0il9NwCx9o=; b=0FtxlnVidlT3q/pSwfJrhH9hTsPG/RoR7OmV7/Rheg74fUAYgPzNfzolVtMtsvUN0x hQm+rZ2uyD1sUnX8KgfdiUcl7aYhFMDUYyg8WMpImcsxEkvRxHZQQKN6HSC5798O+662 xC6tX0dDStjV4QNM4fazLQQlI9ooD18gailrDkKqrt8loTDb80kAPsnIFNBt6QhaRWIx J1JtoPdlUsAPkcVngawqixlJxtMRzAZqYz9aCZRS8aSz7nYkI4rVFvFgwJFQmguEliJ/ 6r1tIXMsKYDFcMequitALwvvfkpUCu1gihrv+jr/F5mVhE7a59sYfhgUxGu5CTGcedF5 glOA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=uyDG0nRE; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2d as permitted sender) smtp.mailfrom=shulman@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=4iL5Kiw7jvRWSjj2hWgApO4ExOWFA0BUI0il9NwCx9o=; b=BphHoG3jLfnvZxIl8oQQX5SaCLXvqWhr7EHhJ4mEySlTO3Ddf/Ppz2RGSpewCvJe8F FLuzYPiDdMBxJUULFuPaM1lums9RbpaxOT1zNSB9Sw+KqfbnT8od9o8OZgqYHsgUWAod GQy0RXfAdxOZ1O1QoopndknJeCPdjRvtpzyhQbQ+NhqLJlrS7Et2y6okJzpWMrOXPDMD o/0R9shTuPd18ati3G8JOzURY6cXNGD3nTi8vVJQJswXBeRuB218fOr3J3leU+ipGN6K Jsaaz8yqMy1J5rkz+SHoAXNgs4oerK4BPsP6O/lFAn6H56aCIRgYAjtqLpDO9fNcgWmf wp8g== 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=4iL5Kiw7jvRWSjj2hWgApO4ExOWFA0BUI0il9NwCx9o=; b=n3TSw+d2faMleWKjpa/puTLnkbwhmw8GZOQqq13So5Mp+M1Lm9i35/V6I66UWCdBcq RcFDKQiseZuJtlMHSp+Xjj9ejJ4yDJxvZQlRFKO2ZbBvIjLBayYmil2j7DoBP9idbEbO uoh4opYu8qF2foPNvHeYgWiskUn/DimCKaBszu1D7R/1690k4BHHT37oPvufip6PSBvT sGJDxvZFcOx9/0FUuolebl4Jcp2pa7Btce1lfj0m0yo+Q2D8HZUPx0/9kfsqjcX4XT5P n1BSqvKXdi5ZtD8+joQownzjwxM8XssIGjeN0lVUCYFZpqNmtwXfT3YxidBsaK5oi9Dc 376w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gI1rdndbhCOnsEn3VGxKrNZAKrdkWwTNkmO6pFBx0hXDmmI59Jd PFey5SJvzrjNRKqFDMaTsuA= X-Google-Smtp-Source: AJdET5dMkXAY1Ncr0T66jGPWBRCgxmJGBMus3KLA1s3s49j/F5hMVVQJQ4W8+LOarRxuHa4JeLyxow== X-Received: by 2002:ae9:c218:: with SMTP id j24-v6mr15718qkg.1.1541620827417; Wed, 07 Nov 2018 12:00:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:bc01:: with SMTP id j1ls841058qvg.1.gmail; Wed, 07 Nov 2018 12:00:27 -0800 (PST) X-Received: by 2002:a0c:81f8:: with SMTP id 53mr985450qve.33.1541620827102; Wed, 07 Nov 2018 12:00:27 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541620827; cv=none; d=google.com; s=arc-20160816; b=HrkZKmkmT1gbbje5fC+2k7d5Lc6DfCu6gwgTuN+0lNQvVRjfVJWaHS8pKgfmknzy9K VdoQuYDUiZ6vFGHNWszIEdZ+3B1KV3OqwUxsjR9XJI9dTcvQifjlDmIfAiGMHF4KNK1N kQWtpPCclefE5EdMwLFt5WUrIL7sxDL9N+vito6CSYAWRQZHU7iQNj5e0JZnhDUKkFUZ RmHTrdQZO6cjGQC0e5wT3F8z9CLoH+/uLlws8Pxt00ziScEhMOaIgMlcNEjSxG+Wtm2D nSvaVlywW3eHTPK/kXWHZ4CnAaExHpO+Iqck4lStNkaMKiimVF6XSSaasdOjrr1/qAx5 ze0Q== 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=j3E7Ehdl0s8N4eFlEoUj5oN2DDT1ApweIJo+nfSMCMg=; b=QdRhcurzZNbubiSur5zvTTuPVd9XTJuYOg7nQr2pdtqyGwKantAI2A2TagNqRI4+xr cc6ley6EootSbi5FwqmssPrfzBr2YaXNQDBk/ClxYxdb9BYf8e+axjt1U3cRSawzDXh4 zSH5OIdPMKfyfazKttarWsBBxHnvAL2Ntmytyi0U48o4XjIHkb3lTsdVsA+B4pc4VEqi rCilFxS4FEseBJ0mUXtoTxtXm1P1rOslPo8Fruz4x0+quIAS+f/mxf71i1M2hyI2m5fA Ck8roPiwSQBTcbkSgYEHU4wH0eDEclR8uZlACTa5xs3n66L1DvnuT3LekyD0ECj4OtQ+ udhA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=uyDG0nRE; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2d as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2d.google.com (mail-yw1-xc2d.google.com. [2607:f8b0:4864:20::c2d]) by gmr-mx.google.com with ESMTPS id 21si93494qkr.2.2018.11.07.12.00.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 12:00:27 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2d as permitted sender) client-ip=2607:f8b0:4864:20::c2d; Received: by mail-yw1-xc2d.google.com with SMTP id z72-v6so7108077ywa.0 for ; Wed, 07 Nov 2018 12:00:27 -0800 (PST) X-Received: by 2002:a0d:d688:: with SMTP id y130-v6mr1646157ywd.132.1541620826368; Wed, 07 Nov 2018 12:00:26 -0800 (PST) Received: from mail-yb1-f178.google.com (mail-yb1-f178.google.com. [209.85.219.178]) by smtp.gmail.com with ESMTPSA id u67-v6sm416211ywd.14.2018.11.07.12.00.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 12:00:23 -0800 (PST) Received: by mail-yb1-f178.google.com with SMTP id z2-v6so7368096ybj.2 for ; Wed, 07 Nov 2018 12:00:23 -0800 (PST) X-Received: by 2002:a25:f80a:: with SMTP id u10-v6mr1718326ybd.219.1541620823193; Wed, 07 Nov 2018 12:00:23 -0800 (PST) MIME-Version: 1.0 References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Wed, 7 Nov 2018 12:00:10 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Peter LeFanu Lumsdaine Cc: Ulrik Buchholtz , HomotopyTypeTheory@googlegroups.com 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=uyDG0nRE; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2d as permitted sender) smtp.mailfrom=shulman@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: , On Wed, Nov 7, 2018 at 6:05 AM Peter LeFanu Lumsdaine wrote: >> As I tried to say, I find that precategory is the novel concept, and tha= t both strict category and univalent category should be familiar to categor= y theorists. (They have a mental model for when one notion is called for or= the other, but we can make the distinction formal.) > > I would argue both are familiar to traditional category theorists. It=E2= =80=99s not unusual to make use of, for instance, the small model for FinSe= t where the set of objects is taken as N =E2=80=94 call this FinSet_N, say.= Category theorists would certainly say that there=E2=80=99s a difference = in character between FinSet_N and FinSet itself: FinSet_N is small; and I t= hink they would also agree that they=E2=80=99re conscious informally of an = extra character FinSet has, which in HoTT can be precisely expressed as its= univalence. > > But do you really think they don=E2=80=99t consider FinSet_N to be a cate= gory?? I find that very hard to believe: I am pretty sure that most tradit= ional category theorists would consider FinSet_N a category without any dou= bt at all, which really seems to imply that the standard concept of categor= y is more like =E2=80=9Cprecategory=E2=80=9D than =E2=80=9Cunivalent catego= ry=E2=80=9D. This is a really interesting question. Traditional category theorists do of course consider FinSet_N to be a category; in particular, it *is* a category according to the definition of "category" in ZFC. One could view this situation as analogous to that of truncated and untruncated Sigmas. When formalizing mathematics in ZFC, there are no untruncated Sigmas. When formalizing mathematics in MLTT, there are no truncated Sigmas. But when formalizing mathematics in HoTT, we have both truncated and untruncated Sigmas. We used to ask the question "when formalizing mathematics in HoTT, should the quantifier 'there exists' be interpreted as a truncated Sigma or an untruncated Sigma?" (This is what led to the somewhat-awkward use of the word "merely" in the book.) But more recently a number of us seem to believe that that's the wrong question, as it presupposes that mathematics has *already* been interpreted into first-order logic, which destroys the *natural* distinction between truncated and untruncated Sigma. Instead we should directly interpret mathematics into HoTT, choosing truncated and untruncated Sigmas as appropriate for the mathematics, without feeling the need to pass through first-order logic. Similarly, when formalizing category theory in ZFC, there are no univalent categories, only strict ones; thus we have to carefully ignore the strictness when working with categories that "should" be univalent. I don't know if there is any foundational theory in which *all* categories are univalent. But when formalizing category theory in HoTT, we have both; and so one might argue that it's wrong to ask whether the word 'category' should refer to strict categories or univalent ones, and instead we should use one or the other as appropriate for the mathematics -- and thus the general word 'category' should refer to something that includes both of them, such as precategories. Is that roughly the point you are making, Peter? I can't deny that there is something to this argument. However, I have two objections to it, or at least to its conclusion. The first is that the analogy breaks down in the following way. The awkwardness of formalizing mathematics in first-order logic comes from *conflating* truncated and untruncated Sigmas. Thus, the problem is solved in HoTT by simply distinguishing them. However, the awkwardness of formalizing category theory in ZFC comes not merely from conflating strict categories with univalent ones, but because doing category theory with strict categories is *intrinsically* awkward, whereas most applications of category theory involve only univalent categories (or more precisely, categories that *should* be univalent), so that awkwardness shouldn't be necessary. I think this is Eric's point: doing category theory with univalent categories is *nicer* than doing it in ZFC, whereas doing category theory with strict categories is *no better* than doing it in ZFC. Why wouldn't we want to emphasize one of the "selling points" of HoTT in our terminology? The strict categories are still there whenever we need them, but giving them a slightly derogatory red-herring adjective is appropriate because they are, for the most part, less well-behaved, and not what the subject of "category theory" is primarily about. My second objection is to the jump from "something that includes both strict and univalent categories" to "precategories". One can argue that traditional category theorists have a notion of "category" that includes both strict categories and univalent categories, but I would argue that their notion does *not* include precategories *other* than strict and univalent ones; instead it is something more like the "union" of strict categories and univalent categories, which is much smaller than the world of precategories. As evidence, I suggest that to a traditional category theorist, the statement "a fully faithful and essentially surjective functor is a (strong) equivalence" is either "just true", "becomes true if you set up the definitions correctly", or "becomes true if you assume the axiom of choice" (depending on the particular category theorist's attitude towards the axiom of choice). In HoTT, this statement for univalent categories is "just true" without any axiom of choice (one way in which doing category theory with univalent categories is nicer), while this statement for strict categories is related to the axiom of choice in exactly the same way as it is in ZFC. But this statement for general precategories is *just false*!! This is easy to see: let Y be any type, considered as a univalent groupoid, let f : X -> Y be any surjection of types, and make X into a precategory in the unique way such that f becomes a fully faithful functor. Then f is also essentially surjective, but for it to be an equivalence the surjection f must have a section; and there are plenty of surjections of types that have no section, such as the inclusion of the basepoint of S^1. So precategories are really weird, and if we define the word "category" to mean "precategory" then category theorists learning about HoTT will see things like this and react "whoa, category theory in HoTT is really weird" -- whereas the correct reaction (when using univalent categories) is "whoa, category theory in HoTT is really awesome"! Moreover, as Ulrik pointed out, there is a notion in traditional (higher) category theory that (under the standard interpretations of HoTT) does coincide with precategories. They're called "flagged categories": https://arxiv.org/abs/1801.08973. In particular, they are *not* called just "categories"! This to me is additional strong evidence that the traditional category theorist's notion of "category" does not include precategories. So if we in HoTT used "category" to mean "precategory", then we would actually be *renaming* something that already exists in traditional mathematics, in a highly confusing way. --=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. For more options, visit https://groups.google.com/d/optout.