From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDN3H5PUGYIJ73ML34CRUBBXL4FSS@googlegroups.com 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=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-ot1-x33f.google.com (mail-ot1-x33f.google.com [IPv6:2607:f8b0:4864:20::33f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 64e363e7 for ; Wed, 7 Nov 2018 14:28:49 +0000 (UTC) Received: by mail-ot1-x33f.google.com with SMTP id x30sf10811335ota.7 for ; Wed, 07 Nov 2018 06:28:48 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Y5mQSDVV7TP9XUt/5msqD8hjsZ4sTzi6LGesrXkFd0w=; b=kfRIZZhDrKb93CUhctTFkERB4GMsNQn82rnr9xsI+6aX/EpuBfmLl+K1jdEyZwwiPI Pe7/qHKcg4wkv+K751RJW9rKePB3MRPd2FJBzorZlK8aZ9m6upDB9vCQEfpwKKXfXSIO XyDN+BPtE0cOFmO59wV/uIqtPPg7QgKW9xwmpMEfQspLnLvlKQp+MVXZlWAP0xdknIiK Ry23Kla2wvXLGvzETydffLE2SAnjL+ZCa3x/zkz2iSnSf/qTsn7XYBd2siCaDuUgFRgz 2GBn50In/UjtzWZVf4eVLJ4R4FmXTCTE3rTus54fTykhqq7MAERbq0lSFZIUzLfEBKvy eXfw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=Y5mQSDVV7TP9XUt/5msqD8hjsZ4sTzi6LGesrXkFd0w=; b=WCc8aajr+6/2qShJLXU/t5XkAPgCKOUzzVZLDwoACI1OCFyF3LX1PaXSpitKd1D59E OIUIbeJpePOle7f3sMnPWGhh0m5i4CV5KRJP35tXL647VD3/ioZFuv/0/k6q5JPe3b/O /NZgQKn2NEJWirhmf+BjIqKmLB9uonZqDv+WyyOCD81646bqiqQL0yFscUo/IGTNzC+4 Ba54iSjmrxA+At2nF3NdRM0VA6HdwP2UzANO2ob6lIjllvfQ/UgrBLEoA2+0eYyEsVmC aEpTkTl7KC+cmz3ZGTP9yy32wrkUBconxeEEQyyCl9RvMDh/FAE1riF7iotkCJM2svy+ SyLg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=Y5mQSDVV7TP9XUt/5msqD8hjsZ4sTzi6LGesrXkFd0w=; b=Woc+rAlWr5rYU2wIVRgpOCLz8oZF4ECncFrgegrqLNB2QoJ2IVX+Vm6FF/BTdsGTIq sRZxa9ObIwRIXC9Syuc5h3fBRMh67bdI2FLOO7G/geG3h7h8VbAqIiffiF9bpymg6uV7 Z006y0y+QNiNAWpNDb5+mvdYZ8t+k8aVpHgpl/+STk323gxRs3O9Jasfx1xp1a7nubr1 9VeT7+Ov1/4zxgT1RMGnxkpV08gL7k7Jwmy6WoAIudjlmtIn4vFVNUtDyGYLqE/agIhH hSuacmQwZjDbtb6MhwCO370bw6qP+KEeYIYHM6MNPz9vUqjDxi/vXJMsKTOCEDeD7CYh iMqg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLkreT9/1Xs9qG1dbChyr89KygC2r6GnhKvifvzvojJunOOUC+Z clLbrFdbPq57H62AMdiRBwE= X-Google-Smtp-Source: AJdET5fUUMt3auwp1wVE/oXhN5QK3K8Agy6wf2GrLe3CTy1swAiM3iDOIFLQBu0wLu5CIkT4L9fIGg== X-Received: by 2002:a9d:fed:: with SMTP id m42mr6931otd.6.1541600927920; Wed, 07 Nov 2018 06:28:47 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:3db4:: with SMTP id l49ls8170487otc.12.gmail; Wed, 07 Nov 2018 06:28:47 -0800 (PST) X-Received: by 2002:a9d:5403:: with SMTP id j3mr6880oth.2.1541600927263; Wed, 07 Nov 2018 06:28:47 -0800 (PST) Date: Wed, 7 Nov 2018 06:28:46 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <4ae4c745-a00e-4ebd-9de2-e29474b75d48@googlegroups.com> In-Reply-To: References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2957_2061117562.1541600926694" X-Original-Sender: UlrikBuchholtz@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: , ------=_Part_2957_2061117562.1541600926694 Content-Type: multipart/alternative; boundary="----=_Part_2958_974565940.1541600926694" ------=_Part_2958_974565940.1541600926694 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Wednesday, November 7, 2018 at 3:05:44 PM UTC+1, Peter LeFanu Lumsdaine= =20 wrote: > > Yep, I indeed meant =E2=80=9Cagnostic=E2=80=9D MLTT =E2=80=94 in particul= ar, without univalence=20 > (or roughly-equivalent things like the glue-types of cubical type theory)= . =20 > There are lots of motivations for working over that as far as possible:= =20 > baking univalence into material where it=E2=80=99s not really required fe= els like=20 > when classical mathematicians make use of AC for no real advantage. > I'm in some respects sympathetic to this. We just have to be aware that=20 working in agnostic type theory leaves us with a burden of=20 mentally/manually handling the relevant notions of identity because the=20 identity types cannot be relied upon. But do you really think they don=E2=80=99t consider FinSet_N to be a catego= ry?? I=20 >> find that very hard to believe: I am pretty sure that most traditional= =20 >> category theorists would consider FinSet_N a category without any doubt = at=20 >> all, which really seems to imply that the standard concept of category i= s=20 >> more like =E2=80=9Cprecategory=E2=80=9D than =E2=80=9Cunivalent category= =E2=80=9D. >> > Well, FinSet_N presents FinSet and we often elide the difference between an= =20 object and a presentation for it, but we do so at our own peril.=20 Traditionally, all categories are presented by a strict category, but=20 traditional category theorists context-switch easily between strict and=20 univalent categories (using heuristics about =E2=80=9Cevil=E2=80=9D=E2=80= =93there we go with the=20 preaching again, sorry!). I'm beginning to despair for ever using the word =E2=80=9Ccategory=E2=80=9D= again without a=20 modifier. The notion of =E2=80=9Cprecategory=E2=80=9D is pretty weird in th= e standard=20 model: Why should the notion of an infinity-groupoid with a family of=20 hom-sets be the sanctified notion?! Of course it turns out to be a useful= =20 notion, just like group presentations are useful. But group theory is about= =20 groups, not group presentations. --=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. ------=_Part_2958_974565940.1541600926694 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Wednesday, November 7, 2018 at 3:05:44 PM UTC+1, Peter = LeFanu Lumsdaine wrote:
Yep, I indeed me= ant =E2=80=9Cagnostic=E2=80=9D MLTT =E2=80=94 in particular, without unival= ence (or roughly-equivalent things like the glue-types of cubical type theo= ry).=C2=A0 There are lots of motivations for working over that as far as po= ssible: baking univalence into material where it=E2=80=99s not really requi= red feels like when classical mathematicians make use of AC for no real adv= antage.

I'm in = some respects sympathetic to this. We just have to be aware that working in= agnostic type theory leaves us with a burden of mentally/manually handling= the relevant notions of identity because the identity types cannot be reli= ed upon.

<= div dir=3D"ltr">
But do you really think they don=E2=80=99t consider FinS= et_N to be a category??=C2=A0 I find that very hard to believe: I am pretty= sure that most traditional category theorists would consider FinSet_N a ca= tegory without any doubt at all, which really seems to imply that the stand= ard concept of category is more like =E2=80=9Cprecategory=E2=80=9D than =E2= =80=9Cunivalent category=E2=80=9D.
=

Well, FinSet_N presents FinSet and we ofte= n elide the difference between an object and a presentation for it, but we = do so at our own peril. Traditionally, all categories are presented by a st= rict category, but traditional category theorists context-switch easily bet= ween strict and univalent categories (using heuristics about =E2=80=9Cevil= =E2=80=9D=E2=80=93there we go with the preaching again, sorry!).
=
I'm beginning to despair for ever using the word =E2=80= =9Ccategory=E2=80=9D again without a modifier. The notion of =E2=80=9Cpreca= tegory=E2=80=9D is pretty weird in the standard model: Why should the notio= n of an infinity-groupoid with a family of hom-sets be the sanctified notio= n?! Of course it turns out to be a useful notion, just like group presentat= ions are useful. But group theory is about groups, not group presentations.=


--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_2958_974565940.1541600926694-- ------=_Part_2957_2061117562.1541600926694--