From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCR53C7ITYGRBOHCRPPQKGQEGPRULUY@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-wr1-x439.google.com (mail-wr1-x439.google.com [IPv6:2a00:1450:4864:20::439]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id fb06a1b5 for ; Wed, 7 Nov 2018 14:05:44 +0000 (UTC) Received: by mail-wr1-x439.google.com with SMTP id u8-v6sf15017042wrn.17 for ; Wed, 07 Nov 2018 06:05:44 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541599544; cv=pass; d=google.com; s=arc-20160816; b=cFzL5Qnq4E8dyaFuR9dBMbcwHkcu85BsMrnDCE3BWmBoVain7BwZVk7oQpatLt5vRn 8wYizB2inxs/ioRzu0kvqLwetmmQBYXhD/CxHrKtJNu3mrdl3VKJ+j3RDxe4BD4wuban x5ghrQjndC9dU69/Vzj5TBqMfjTMsHBHJxATjihWymswcm/zeFEa/UZiEqmHGTpSwzLx PdmfAuuC2Nih32t3NphszvYnX6Mad8y9UL43y70pEsbfzNum2FQRCvXotCHQp5La0QfS X5P6HhB9voV6Jyr5SMPLURE+PPc9mC58HsYLUfzid+Ig6/UpPjLMfmeddREho3lgIjh8 HqAw== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=HK4UiZoxVPoYThwuPed/hgw5dVbDe8x9bR8LLJJgJ5U=; b=eoohh86+qMJ4c/+8Pt0z9vzPWg3wPCFbSdWSHk2FWJouQoEJWN5F1T3IYtfHHX+HJS SAOZI5jlZ54uz1eMwXbbBjYitcCCn1POC6N3KGfLr02iPIOSTfsMpwqYMYCiLEu3f3nX kNGfH19lipke5jW3RO8Nkvps75+PThwb8mjLcgoMObK/JTnLqbJRbE76iNdT100bNS9N 4s5XzrSTmmZmnMRsg9CyPlv0/pGIYy1BXPPypgM/3+0aXWZba6A92MRrKVuV9s8DPn8b lcN0ko0dJA/z5NJLqwLLy9+1AewdxMF6DHuwRjG09RbFRKMz+TJZKDvQ4tBwQJD2N4i0 B2Xw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=DoMy1Jqj; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) smtp.mailfrom=p.l.lumsdaine@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:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=HK4UiZoxVPoYThwuPed/hgw5dVbDe8x9bR8LLJJgJ5U=; b=pbiMrab7v2x8V/OtFt7HgJw7dyoXXUEeYRwdLwceNqaLxM5YUPMPu2GQs3cuF5ReT3 v/AN5vAG1Goy0XOOo8epgQejQLT9/CvQ8WgBaba83VSo6KMqKwEm7eY4T6rJ1b80ZpMo DRjIDqtZB2VnvfCz/gjwFVvo2oX5/LADox2yFcTl/R4Vd27QwKY4+6Yq1gKgyHUTRmfc qsuAKhUdkDze9Ci/BlDtNpzp382ivrXuiOY/n/DhazPVmGBsCyQmNjM+rp3v1dnGeEX9 kpamq3gmIYeWvjOtW6jIgztAfjGFIYqPkNGsDrhE2V6HYUcHxELnQseTp0Ttaoo+QwKi xJng== 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 :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=HK4UiZoxVPoYThwuPed/hgw5dVbDe8x9bR8LLJJgJ5U=; b=L8k6gQHfFihciujpqaDLuc09lI9zG0+YL7EMVRKhRemVaCGm0lh+c1bSSv1oO57y64 D5H6dPPnH79Fqxy1fbXQq48u7kEUBW7OstV+KewgAjmAL27P4w96pcr7uG4u/hKwKdqY d8ShwJcgHt027IoQKjdSCgaoxx6s9oDaqnah3rZGgWalp8f/1z/jWfWZBKoMSnOvaS7V y0pGdeF5li1Uxp3pF3XhBUKLoVqAVATderUhVUpaWoLKYr1xJfLAOafKMb4Tpvhy30d0 tAlO2pHX5LOOTpb6Qu7vjS+wJvXaqsTcJmdn11cTDCJM9ow4rbVVn6RPuvROXwXCEvkb rkJA== 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: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=HK4UiZoxVPoYThwuPed/hgw5dVbDe8x9bR8LLJJgJ5U=; b=TeLUWq85aAUzyNQZky3W+eRNRCJnXUmfON5m2xd3xjfday/msidb8gwsg2fLcSDKbY LQis+mUQdC9auRAi/ZtjeYY1wPrOmob+kmiQLADiTqBfjWMSWe/fMp17EJZAnWDiOvfl 3y1O+LePiUse+cx0dRBAUoLUlUwZAUWokKWEbE8u1E1i9+x/0EALcqbIUqaMujjLB6hr kqkQ3kcKBLJaL92VYuO5BmffsbK8RlaUwPY+XDB85kstweR+rI5EHwxbSkqNQ0xJ5u+l 00Tlgqg4T4Dv1IJrjXWHUYGray2Derc7ikf0n9xM2egOdqKkx+i1kqfRAYqDgFNLRWd6 ACDg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gK+pcmfbSilQdXJnaE0JgnqhgLxRTLFU6Wcc7/+u+obrUO4p5+/ DAX1ll72B2BA/6ohC4v0ymQ= X-Google-Smtp-Source: AJdET5fpy6oYdVTGAd324MaMZZAAlbeXriPSHcUNzw58u5kb2rEfaorW5nptco+YmukYEyinFoe0UQ== X-Received: by 2002:adf:fdc3:: with SMTP id i3-v6mr4592wrs.2.1541599544186; Wed, 07 Nov 2018 06:05:44 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:da01:: with SMTP id r1-v6ls2612152wmg.24.gmail; Wed, 07 Nov 2018 06:05:43 -0800 (PST) X-Received: by 2002:a1c:cc9:: with SMTP id 192-v6mr73052wmm.8.1541599543558; Wed, 07 Nov 2018 06:05:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541599543; cv=none; d=google.com; s=arc-20160816; b=qT7mm6C67SOnZu5nptqDDWic/veRksWoZbqeplluOV9mbWwogqZSUnkNnfKuwc2Bry QtingtoNqfi+PJ8CTqmgtW3nbA/RDoDo8PCMXbQJldQqpGCCl5KSfr5cR1dQVC15kp9D J46qouX9pK4wQQ7fsid2Ta8ycd0l1b9IU/F3oejsDZK/TkYC2gQLyX5C8iebw+JiEHa/ Brav2ZqmUQpaeilN0Sm/limn4ItSgWOd3PXBeBsdQmVHBHN1Qtl0evYi3oJ5/pq2vvho DPC83hDpBm44225Gi+Z6whEcNxG7Kt6sS1EI3cena+/Ft5MFjQ4TlkpBcIMfBf3q9/10 9HpQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=c5WWZum54Cx74SQtxDvY7CLGZT9XNXZJhW6hEUsBU0Q=; b=CxZ19htPSKa+3nWMDg/U9f5s6jRC/Dn3ml7SMpltOYXgJ6oj5oHXRQ3UarDpTN/S4/ s2S2oN3wz/euEEsmQ2rkQfRQ7RQ8ChSSxtMBdN+SP8RTYElZTH0a9cNjnOIvBqaFH5ec K3kjKXQ5PxvBhsWG/aJVjy8ER0ecJJ2WQzbu9o9PUqrIEyB9Jh5Uj+tS08ERhjVlCMwz VAQhcmtoZGzF2P3xeR+DBM/JuvUhxFuSPrWYduEQAMYhEQRxEbUCq4T1GnlEw4rXD/nV EcdqOHWdX1R0EUN4aJKVJKWdH7W5FoHkRR+lhIaI+K1xCzKqb/3Lfv2NYwar1bzpOE+2 oCNw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=DoMy1Jqj; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) smtp.mailfrom=p.l.lumsdaine@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x529.google.com (mail-ed1-x529.google.com. [2a00:1450:4864:20::529]) by gmr-mx.google.com with ESMTPS id h137-v6si46009wmd.1.2018.11.07.06.05.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 06:05:43 -0800 (PST) Received-SPF: pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) client-ip=2a00:1450:4864:20::529; Received: by mail-ed1-x529.google.com with SMTP id c25-v6so13486065edt.8 for ; Wed, 07 Nov 2018 06:05:43 -0800 (PST) X-Received: by 2002:a50:90fb:: with SMTP id d56-v6mr312140eda.228.1541599543188; Wed, 07 Nov 2018 06:05:43 -0800 (PST) MIME-Version: 1.0 References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> In-Reply-To: <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> From: Peter LeFanu Lumsdaine Date: Wed, 7 Nov 2018 15:05:31 +0100 Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Ulrik Buchholtz Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000286003057a139dd3" X-Original-Sender: p.l.lumsdaine@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=DoMy1Jqj; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::529 as permitted sender) smtp.mailfrom=p.l.lumsdaine@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: , --000000000000286003057a139dd3 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Wed, Nov 7, 2018 at 12:43 PM Ulrik Buchholtz wrote: > I'm a bit confused by your message, Peter: HoTT doesn't have a naive set > interpretation and is inconsistent with UIP, so I'm not sure how that > should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) > Yep, I indeed meant =E2=80=9Cagnostic=E2=80=9D MLTT =E2=80=94 in particular= , without univalence (or roughly-equivalent things like the glue-types of cubical type theory). There are lots of motivations for working over that as far as possible: baking univalence into material where it=E2=80=99s not really required feel= s like when classical mathematicians make use of AC for no real advantage. As I tried to say, I find that precategory is the novel concept, and that > 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 FinSet where the set of objects is taken as N =E2=80=94 call this FinSet_N, say. Catego= ry theorists would certainly say that there=E2=80=99s a difference in characte= r between FinSet_N and FinSet itself: FinSet_N is small; and I think they would also agree that they=E2=80=99re conscious informally of an extra char= acter 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 catego= ry?? I find that very hard to believe: I am pretty sure that most traditional category theorists would consider FinSet_N a category without any doubt at all, which really seems to imply that the standard concept of category is more like =E2=80=9Cprecategory=E2=80=9D than =E2=80=9Cunivalent category=E2= =80=9D. =E2=80=93p. --=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. --000000000000286003057a139dd3 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Wed, Nov 7, 2018 at 12:43 PM Ulrik Buc= hholtz <ulrikbuchholtz@gmail= .com> wrote:
I'm a bit confused by your message, Peter: HoTT doesn't ha= ve a naive set interpretation and is inconsistent with UIP, so I'm not = sure how that should guide us. (Maybe if we're working in good old (agn= ostic?) MLTT?)

Yep, I indeed meant = =E2=80=9Cagnostic=E2=80=9D MLTT =E2=80=94 in particular, without univalence= (or roughly-equivalent things like the glue-types of cubical type theory).= =C2=A0 There are lots of motivations for working over that as far as possib= le: baking univalence into material where it=E2=80=99s not really required = feels like when classical mathematicians make use of AC for no real advanta= ge.

As I tried to say= , I find that precategory is the novel concept, and that both strict catego= ry and univalent category should be familiar to category theorists. (They h= ave a mental model for when one notion is called for or the other, but we c= an make the distinction formal.)

I wo= uld argue both are familiar to traditional category theorists.=C2=A0 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.= =C2=A0 Category theorists would certainly say that there=E2=80=99s a differ= ence in character between FinSet_N and FinSet itself: FinSet_N is small; an= d I think they would also agree that they=E2=80=99re conscious informally o= f an extra character FinSet has, which in HoTT can be precisely expressed a= s its univalence.

But do you really think they don= =E2=80=99t consider FinSet_N to be a category??=C2=A0 I find that very hard= to believe: I am pretty sure that most traditional category theorists woul= d consider FinSet_N a category without any doubt at all, which really seems= to imply that the standard concept of category is more like =E2=80=9Cpreca= tegory=E2=80=9D than =E2=80=9Cunivalent category=E2=80=9D.

=E2=80=93p.

--
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.
--000000000000286003057a139dd3--