From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDN3H5PUGYIM3I4L34CRUBGURJS2S@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-oi1-x23a.google.com (mail-oi1-x23a.google.com [IPv6:2607:f8b0:4864:20::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 964dd0f8 for ; Wed, 7 Nov 2018 11:51:42 +0000 (UTC) Received: by mail-oi1-x23a.google.com with SMTP id l204-v6sf10486377oia.17 for ; Wed, 07 Nov 2018 03:51:42 -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=kZesvieTailF69q5PU45XNlxsgsqzqTe2ibd8/x69fc=; b=DKClbww17kSafPWALsjM2R+lEkZ0K4X/MGYmIlUjlA/N+rMaoq/t7dwXINKRmfwZvF 8VAMMBAJLRViepNrPq5I02Os4AMmQhpd3PjPX4q+Qm9Kw7YZwkNdMvQmpJ8QOqGNPr1Q C130won+OX6Mw9w/OjkV1mgy2oVsdxyZCvLrku3vzuq7JcjWFtURx0voxg8TQjCdOExm 5MUYRj9M4r0c9F/DP/nuMtOYMpzRF9BpzIzdIilglpTbLLLDwdlfdNtWpTGhGwFuEBNJ 6mCVyAVb/atwmrOVn7CE4KVeefGwIWaA5X3U3G7Qb/P4AV2HUYzPgxyQ9eAV+yNuyqsT 888A== 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=kZesvieTailF69q5PU45XNlxsgsqzqTe2ibd8/x69fc=; b=nHYK3Fq2Hv22x9jkXwggKCuoCS7ohIA5js09A+mcTqjQWtIj0xgu7qITPOdiwiXDPr Jg31fDgD+Qt0EFjne7kBw2OtPIfe82go2iOfG/gJt3B+EdBiw9MV18uoxRvoeN4WXXom ydkkg0mvFNM1gXIJ9MkZVwO5mYHVH6CniQMZ4aa3upS4mq/rAI2eExJH8A246sg3oSFh A9dngaaav6IGL9quXawJLuAwMooxeBTYcV7yQwNCrMUCr4FdzhqzTDQaHxJ48btwShn+ SM+IL+iekEm81y9fA9lbqyI3ZxE1gAO+WZxSgLaUmmR9r8Sesg455cvAZvaaUkbWB+1q CWsw== 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=kZesvieTailF69q5PU45XNlxsgsqzqTe2ibd8/x69fc=; b=JmTNptmD7SBLz4iqrQRUe7w/bXLfK5jEMHX5cy4dw2Y7174kNdBdmjIk0kqIPXscwt ra9ApWJwJrtI7OU7fs1zf4ZCYSeYdvFYB0QUBhO2P9EwF3emzLLkM31zAslLGCAPedGO i3uxIpZ2zs3SdQrj6CE/I/8+M0RE7Ah1i8S9DYft76GHB6+11YGnC4OLqpNSyECgoicp aqTTySLYYYKFQOmx7uNM/W1gyLFQuSU0O8NUbVb2M5vsm24TUF/nBTyJpfQU/Hq5qURe 3z9KBrViJnPQ8U+92OI5FyqXRmI4Nr8St/DcgpUKO8qk/uJV6NQlpFXhi5/8HhyjVOZJ sBWw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLWMDSgATIsjt2hnVKRhLxGgPNdTTmmbj5k4UBvjgkDXLUaMdVX IunN6RWeEq2TPkt4Yea7hDc= X-Google-Smtp-Source: AJdET5f1enJcPd8/dJ/Oy/5a3j2/rezriIdX2jNeJdOdfhUN2zHEsLT64OGYdqXjkM+nHG2LXq6+Dw== X-Received: by 2002:aca:ad0a:: with SMTP id w10-v6mr36071oie.2.1541591501430; Wed, 07 Nov 2018 03:51:41 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2cd5:: with SMTP id e21ls7117386otd.0.gmail; Wed, 07 Nov 2018 03:51:41 -0800 (PST) X-Received: by 2002:a9d:3d06:: with SMTP id a6mr30921otc.0.1541591501077; Wed, 07 Nov 2018 03:51:41 -0800 (PST) Date: Wed, 7 Nov 2018 03:51:40 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <706ac90f-ebd1-49f8-bd0c-2029549373c3@googlegroups.com> In-Reply-To: <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> 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_2368_288645649.1541591500541" 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_2368_288645649.1541591500541 Content-Type: multipart/alternative; boundary="----=_Part_2369_1102840759.1541591500541" ------=_Part_2369_1102840759.1541591500541 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Let me add one more point: in agnostic type theory, we can't define the=20 type of (Cauchy) real numbers, so we make do with the setoid of Cauchy=20 sequences. Likewise, we can't define the type of (univalent) categories, so= =20 we make do with the 2-groupoid of precategories, equivalences and natural= =20 isomorphisms. In agnostic type theory we are both in setoid and higher groupoid hell. In= =20 set theory/extensional type theory, we can escape the setoid hell, but=20 still have the higher groupoid hell, and in HoTT we can finally escape this= =20 particular family of infernos :) On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ulrik Buchholtz wrote: > > I'm a bit confused by your message, Peter: HoTT doesn't have a naive set= =20 > interpretation and is inconsistent with UIP, so I'm not sure how that=20 > should guide us. (Maybe if we're working in good old (agnostic?) MLTT?) > > As I tried to say, I find that precategory is the novel concept, and that= =20 > both strict category and univalent category should be familiar to categor= y=20 > theorists. (They have a mental model for when one notion is called for or= =20 > the other, but we can make the distinction formal.) > > On Wednesday, November 7, 2018 at 12:10:10 PM UTC+1, Peter LeFanu=20 > Lumsdaine wrote: >> >> Ulrik=E2=80=99s email nicely lays out the three key notions (pre-categor= y, strict=20 >> category, univalent category), and the argument for the=20 >> Ahrens=E2=80=93Kapulkin=E2=80=93Shulman / HoTT book terminology, with = =E2=80=9Ccategory=E2=80=9D meaning=20 >> =E2=80=9Cunivalent category=E2=80=9D by default. >> >> For my part I lean the other way: I think it=E2=80=99s too radical to us= e=20 >> =E2=80=9Ccategory=E2=80=9D for a definition which doesn=E2=80=99t come o= ut equivalent to the=20 >> traditional definition under the na=C3=AFve set interpretation (or under= the=20 >> addition of UIP to the type theory). Choosing terminology that actively= =20 >> clashes with traditional terminology makes it much harder to compare=20 >> statements in HoTT with their classical analogues, and see what differen= ce=20 >> HoTT really makes to the development of topics. >> >> Based on that criterion, I strongly prefer taking category to mean=20 >> =E2=80=9Cprecategory=E2=80=9D. A big payoff from this is that if you fo= rmalise something=20 >> using =E2=80=9Ccategory =E2=80=9D to mean =E2=80=9Cprecategory=E2=80=9D = in type theory without assuming UA,=20 >> then you can read the result either as valid in HoTT, or (under the=20 >> set-interpretation) as ordinary arguments in classical category theory,= =20 >> with all the terms meaning just what they traditionally would. >> >> Univalence of categories is an important and powerful property, but not= =20 >> an innocuous one; it changes the character of the resulting =E2=80=9Ccat= egory=20 >> theory=E2=80=9D in interesting ways. Making the restriction to univalen= t=20 >> categories tacit is misleading to readers who aren=E2=80=99t fully =E2= =80=9Cinsiders=E2=80=9D, and=20 >> obscures understanding its effects. >> >> =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. ------=_Part_2369_1102840759.1541591500541 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Let me add one more point: in agnostic type theory, we can= 't define the type of (Cauchy) real numbers, so we make do with the set= oid of Cauchy sequences. Likewise, we can't define the type of (univale= nt) categories, so we make do with the 2-groupoid of precategories, equival= ences and natural isomorphisms.

In agnostic type theory = we are both in setoid and higher groupoid hell. In set theory/extensional t= ype theory, we can escape the setoid hell, but still have the higher groupo= id hell, and in HoTT we can finally escape this particular family of infern= os :)

On Wednesday, November 7, 2018 at 12:43:32 PM UTC+1, Ul= rik Buchholtz 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?)

As I tried to say, I find that precategor= y is the novel concept, and that both strict category and univalent categor= y should be familiar to category theorists. (They have a mental model for w= hen one notion is called for or the other, but we can make the distinction = formal.)

On Wednesday, November 7, 2018 at 12:10:10= PM UTC+1, Peter LeFanu Lumsdaine wrote:
Ulrik=E2=80=99s email nicely lays out the three key n= otions (pre-category, strict category, univalent category), and the argumen= t for the Ahrens=E2=80=93Kapulkin=E2=80=93Shulman / HoTT book terminology, = with =E2=80=9Ccategory=E2=80=9D meaning =E2=80=9Cunivalent category=E2=80= =9D by default.

For my part I lean the other way: I thin= k it=E2=80=99s too radical to use =E2=80=9Ccategory=E2=80=9D for a definiti= on which doesn=E2=80=99t come out equivalent to the traditional definition = under the na=C3=AFve set interpretation (or under the addition of UIP to th= e type theory).=C2=A0 Choosing terminology that actively clashes with tradi= tional terminology makes it much harder to compare statements in HoTT with = their classical analogues, and see what difference HoTT really makes to the= development of topics.

Based on that criterion, I= strongly prefer taking category to mean =E2=80=9Cprecategory=E2=80=9D.=C2= =A0 A big payoff from this is that if you formalise something using =E2=80= =9Ccategory =E2=80=9D to mean =E2=80=9Cprecategory=E2=80=9D in type theory = without assuming UA, then you can read the result either as valid in HoTT, = or (under the set-interpretation) as ordinary arguments in classical catego= ry theory, with all the terms meaning just what they traditionally would.

Univalence of categories is an important and powerf= ul property, but not an innocuous one; it changes the character of the resu= lting =E2=80=9Ccategory theory=E2=80=9D in interesting ways.=C2=A0 Making t= he restriction to univalent categories tacit is misleading to readers who a= ren=E2=80=99t fully =E2=80=9Cinsiders=E2=80=9D, and obscures understanding = its effects.

=E2=80=93p.

<= /div>

--
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_2369_1102840759.1541591500541-- ------=_Part_2368_288645649.1541591500541--