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=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-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 23ff2ff6 for ; Thu, 8 Nov 2018 21:37:23 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id p29sf6838895ote.3 for ; Thu, 08 Nov 2018 13:37:22 -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=SE5V6KiuCVnNp8q6b6efYXiS7x7qFFJc59mtnnrgCsg=; b=H2t8R5qOKZEYsFj0K8fWmoYxAi02f2Wb82KYwV8Ir6px2kXiMBPTvEXyqVC2FnEBdL PH9PYZRFrizhjh6rekgKeHcU8zWO9+CcAI/cCCdY1l9xqmTKuLCuQ2A0TOdpMuDuYlPF uyeZ9V4J0HNoMfcfmqaW40AD/eLhSSclYZXX7n8AHXkITqbB0G6Jncgw3/QPXviFEKLf LP5Abp74PIU3S28l84hHXk1mYQe5UcPNVzovqdTJvUfeYTdeU3qGepewqLEjY19XSQz6 JpJeErOt+TR0buKJhVazPNm1JCsK9xvZ9kdX9/9eVWWoRN/zXP+VH4ZhUWspNPhgAAy4 HAfA== 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=SE5V6KiuCVnNp8q6b6efYXiS7x7qFFJc59mtnnrgCsg=; b=oEGh+I/ZbyfwT27zNVGswJgcWyDO7WV6uFd4jy9Bprg+0sHRvjdMUeJVFrG2jomEkl SWDqzi8SlCXJbUgZXaFkgPsbtJyNMnoR58Ch+t0dr0/qQqfoE5nWASUs/+ZmZXkzFKvF yQ193I06824kC4t+YArqoCSJh5c4anKfQyNM8kGPJtp1wFX+dKrGN/LabMqSJY2pT/eW tOnudxvdIOLioZDrZ50hKv9IGnjCRmgcSxercWbqnWaG594D9aTUCkUCuSigBX0j+hfv btQFf0CasGa0j0AtNdFzs6JKyp+wkfpeechx9IUvbw5/rnMKXXQQBM+lGkQJyKKm735P ajMg== 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=SE5V6KiuCVnNp8q6b6efYXiS7x7qFFJc59mtnnrgCsg=; b=XsOP6uuaJZpNnegMuKe+pSKsbCZDEhYItm/VylgKhu3ghyReRtYUzW3dADPt/aEtqJ f7qfNogABl6znl8wp3kEfmns7hwPXDHgsQHR/H3+jNHay5cApJM9ZvNyKeUofMcabkd2 e2CDKYxa4Mp56Eyx/k9p8noHlEdJ7pmqQw7kEWw7THOzBerBHheqCHgLoGMGa3wUUff5 zAt5BTHSLGB0J0BdWcSPLEp7SCgz9s+AnpSX/nashHCvDc9XrNS9r3bsDa7M8VDtMZ1a f8D2Rmf3Avu41f0EJkLrtOarPudU3j3cKS/kigXGs2PGe06vi0ThjQyB1nQVxR6bf0QS 5XUg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gL1ulU5wp2F7IKtLQ5E8Jm0m+xy4AugxuulLSPafMZi5NDzq7sz Der38oX2yJesUEtq81NjMRM= X-Google-Smtp-Source: AJdET5fqWiMMQo9W9DIzNWdr2oXt4AGp0IMZR/zS2fRn23zc8mtf0Rq4vMQifZsmrXC/pg+JNTxVKA== X-Received: by 2002:a9d:bd5:: with SMTP id 79mr103976oth.7.1541713041888; Thu, 08 Nov 2018 13:37:21 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:768b:: with SMTP id j11ls1389537otl.5.gmail; Thu, 08 Nov 2018 13:37:21 -0800 (PST) X-Received: by 2002:a9d:43:: with SMTP id 61mr107961ota.3.1541713041238; Thu, 08 Nov 2018 13:37:21 -0800 (PST) Date: Thu, 8 Nov 2018 13:37:20 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <5645fcc6-2520-498f-8e82-0b335d4eb3f1@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_706_1396157426.1541713040631" X-Original-Sender: escardo.martin@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_706_1396157426.1541713040631 Content-Type: multipart/alternative; boundary="----=_Part_707_353805176.1541713040631" ------=_Part_707_353805176.1541713040631 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We have two separate issues here: (1) What is the appropriate notion of category for univalent mathematics. (2) What is the right terminology for it. There is also a separate, orthogonal question, (3) Whether there is a foundation-independent (dubbed "agnostic") notion of category, which gives the right notion for each foundation, *and* can be formulated in MLTT (without K or univalence). Regarding (3), even if this is possible (assuming the question makes sense), it is not given by any of the proposed notions, and this should not be regarded as surprising or shocking. (This raises the question of whether there is a categorical definition of category, for people who would like to see category theory itself as a foundation.) Regarding (1), I think the arguments by Ulrik, Paolo, Mike and Eric (Finster) are pretty convincing: "univalent category" is the right notion of category for univalent mathematics. However, it *is* common and useful in mathematics to formulate and prove theorems with minimal hypotheses, and then what is called a pre-category, and what Thorsten called a wild category, often arise naturally and unavoidably as part of the building blocks of mathematics. Regarding (2), I would say, in view of (the answer to) (3), that it is probably better to avoid the naked terminology "category" in HoTT/UF, as it would give the wrong impression of *capturing* a universal, pre-existing, foundation-independent notion of category (in particular compatible with the ZFC view of what a category is, which has evilness as a built-in feature): * Then "univalent category" could mean, ambiguously but consistently, both (a) a pre-category that satisfies a certain technical condition analogous to the univalence axiom for types, or (b) "the appropriate notion of category for univalent mathematics". (c) In both cases, (a) and (b), the adjective "univalent" makes sense. In (b), it would be not in opposition to "category", but instead in opposition to e.g. "ZFC category". Martin On Wednesday, 7 November 2018 15:55:45 UTC, Michael Shulman wrote: > > I strongly agree with Ulrik. Perhaps the point that's not getting=20 > across is that we are not talking about terminology for MLTT in=20 > general, but specifically for HoTT (with univalence). The terminology=20 > to be decided on doesn't have to make sense or come out to anything=20 > meaningful in type theory with UIP, and we shouldn't expect it to.=20 > The terminology in MLTT+UIP should be different from that for MLTT+UA,=20 > because they are different theories and relate to "traditional"=20 > mathematics in different *incompatible* ways. I doubt there is *any*=20 > choice of terminology for plain MLTT without UA *or* UIP that is=20 > sensible in that it can be specialized to the right terminology upon=20 > the addition of either of these two inconsistent axioms.=20 > On Wed, Nov 7, 2018 at 6:27 AM Peter LeFanu Lumsdaine=20 > > wrote:=20 > >=20 > > On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz > wrote:=20 > >>=20 > >> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirc= h=20 > wrote:=20 > >>>=20 > >>> As I tried to say, I find that precategory is the novel concept, and= =20 > that both strict category and univalent category should be familiar to=20 > category theorists. (They have a mental model for when one notion is call= ed=20 > for or the other, but we can make the distinction formal.)=20 > >>>=20 > >>>=20 > >>> This is too clever!=20 > >>>=20 > >>>=20 > >>>=20 > >>> If you just transcribe the traditional definition of a category in=20 > type theory you end up with what in the HoTT book is called precategory.= =20 > This is confusing for the non-expert even though you can justify why it= =20 > should be so.=20 > >>=20 > >>=20 > >> No, you get the notion of a strict category, which in some sense is al= l=20 > that you directly have in set theory.=20 > >=20 > >=20 > > No in turn: you can arguably get either strict categories, or=20 > precategories, or what Thorsten dubbed =E2=80=9Cwild categories=E2=80=9D = above, since =E2=80=9Cset=E2=80=9D=20 > in set theory is the (na=C3=AFve) interpretation of both =E2=80=9Cset=E2= =80=9D and =E2=80=9Ctype=E2=80=9D.=20 > (Just as when you transcribe classical definitions in a constructive=20 > setting, you sometimes want to read =E2=80=9Cpredicate=E2=80=9D just as = =E2=80=9Cpredicate=E2=80=9D and=20 > other times as =E2=80=9Cdecidable predicate=E2=80=9D =E2=80=94 all predic= ates are decidable=20 > classically, but that doesn=E2=80=99t mean that their constructive transc= ription=20 > should include =E2=80=9Cdecidable=E2=80=9D by default.)=20 > >=20 > > =E2=80=93p.=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send= =20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com = .=20 > > > For more options, visit https://groups.google.com/d/optout.=20 > --=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_707_353805176.1541713040631 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
We have two separate issues here:

(1) What is the appropriate notion of category for univalent
mathematics.

(2) What is the right terminology f= or it.

There is also a separate, orthogonal questi= on,

(3) Whether there is a foundation-independent = (dubbed "agnostic")
notion of category, which gives the= right notion for each
foundation, *and* can be formulated in MLT= T (without K or
univalence).

Regarding (= 3), even if this is possible (assuming the question
makes sense),= it is not given by any of the proposed notions, and
this should = not be regarded as surprising or shocking.

(This r= aises the question of whether there is a categorical
definition o= f category, for people who would like to see category
theory itse= lf as a foundation.)

Regarding (1), I think the ar= guments by Ulrik, Paolo, Mike and
Eric (Finster) are pretty convi= ncing: "univalent category" is the
right notion of cate= gory for univalent mathematics.

However, it *is* c= ommon and useful in mathematics to formulate
and prove theorems w= ith minimal hypotheses, and then what is
called a pre-category, a= nd what Thorsten called a wild category,
often arise naturally an= d unavoidably as part of the building
blocks of mathematics.

Regarding (2), I would say, in view of (the answer to)= (3), that
it is probably better to avoid the naked terminology &= quot;category"
in HoTT/UF, as it would give the wrong impres= sion of *capturing*
a universal, pre-existing, foundation-indepen= dent notion of
category (in particular compatible with the ZFC vi= ew of what a
category is, which has evilness as a built-in featur= e):

=C2=A0 =C2=A0 =C2=A0* Then "univalent cat= egory" could mean, ambiguously but
=C2=A0 =C2=A0 =C2=A0 =C2= =A0consistently, both

=C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 (a) a pre-category that satisfies a certain technical
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 condition analog= ous to the univalence axiom for
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 types, or

=C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 (b) "the appropriate notion of category fo= r univalent
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0mathematics".

=C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 (c) In both cases, (a) and (b), the
=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 adjective "univalent&= quot; makes sense. In (b), it
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 would be not in opposition to "category", bu= t
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 instead= in opposition to e.g. "ZFC category".

M= artin


On Wednesday, 7 November 2018 15:55:45 UTC, M= ichael Shulman wrote:
I strong= ly agree with Ulrik. =C2=A0Perhaps the point that's not getting
across is that we are not talking about terminology for MLTT in
general, but specifically for HoTT (with univalence). =C2=A0The termino= logy
to be decided on doesn't have to make sense or come out to anything
meaningful in type theory with UIP, and we shouldn't expect it to.
The terminology in MLTT+UIP should be different from that for MLTT+UA,
because they are different theories and relate to "traditional&quo= t;
mathematics in different *incompatible* ways. =C2=A0I doubt there is *a= ny*
choice of terminology for plain MLTT without UA *or* UIP that is
sensible in that it can be specialized to the right terminology upon
the addition of either of these two inconsistent axioms.
On Wed, Nov 7, 2018 at 6:27 AM Peter LeFanu Lumsdaine
<p.l.lu...@gmail.com> wrote:
>
> On Wed, Nov 7, 2018 at 3:14 PM Ulrik Buchholtz <ulrikbu...@gmail.com= > wrote:
>>
>> On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten A= ltenkirch wrote:
>>>
>>> As I tried to say, I find that precategory is the novel co= ncept, and that both strict category and univalent category should be famil= iar to category theorists. (They have a mental model for when one notion is= called for or the other, but we can make the distinction formal.)
>>>
>>>
>>> This is too clever!
>>>
>>>
>>>
>>> If you just transcribe the traditional definition of a cat= egory in type theory you end up with what in the HoTT book is called precat= egory. This is confusing for the non-expert even though you can justify why= it should be so.
>>
>>
>> No, you get the notion of a strict category, which in some sen= se is all that you directly have in set theory.
>
>
> No in turn: you can arguably get either strict categories, or prec= ategories, or what Thorsten dubbed =E2=80=9Cwild categories=E2=80=9D above,= since =E2=80=9Cset=E2=80=9D in set theory is the (na=C3=AFve) interpretati= on of both =E2=80=9Cset=E2=80=9D and =E2=80=9Ctype=E2=80=9D. =C2=A0(Just as= when you transcribe classical definitions in a constructive setting, you s= ometimes want to read =E2=80=9Cpredicate=E2=80=9D just as =E2=80=9Cpredicat= e=E2=80=9D and other times as =E2=80=9Cdecidable predicate=E2=80=9D =E2=80= =94 all predicates are decidable classically, but that doesn=E2=80=99t mean= that their constructive transcription should include =E2=80=9Cdecidable=E2= =80=9D by default.)
>
> =E2=80=93p.
>
> --
> 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.
> For more options, visit https://groups.go= ogle.com/d/optout.

--
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_707_353805176.1541713040631-- ------=_Part_706_1396157426.1541713040631--