From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDN3H5PUGYIOLH4L34CRUBD2SDPI4@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-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1e350a19 for ; Wed, 7 Nov 2018 11:43:34 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id g28sf8216912otd.19 for ; Wed, 07 Nov 2018 03:43:34 -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=tIkw7Yhz1fDobLruZQ9dGfevX+0YNoWbemi0+agaonw=; b=jc9mUBrX9mg6kgJmcV2KxDrSjxby3Hdb9U5rvcITOUhg1hNaG593RtIbEOLuNefRzM H5lCrJPdKt/sDjH+B1DJdejlrevLHvo3kPdtF92Tv9FdNmWYqoyCKjL9VDYc6raXtGuh pFSmzRK3QSGBG997xp20VSJE9q4CacXLdc4E/DszzPVCIOns7qz+J53NcbRDr3A+YEvd SP1Kks7ZOx2cUrXzaalBjrhMkqS1C46jompbtjYXPwoJ8NlUL1qXDfgLU8QZq5XacHm7 mnnG9YvVMt04BYV/O9Nz9KpG6PxfSKaKkNHXDmkAipZlcmE+ay1ZZV6Ig4ZStgl3lab4 M0mw== 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=tIkw7Yhz1fDobLruZQ9dGfevX+0YNoWbemi0+agaonw=; b=le7vpVJCJl7NZ2TmMlqyYknVyvnQaR9D6hi8MQE6/hOtGEPbWWkIbHUCDN2Ul2M/6u uoqAoTP2gMBSjEJTX17hFNHpo8JLH8ghWcA3Dez7Dsh2S9IEbEIf4OKbfBEtz8QBRwm6 AXQC45GfE7qy3rHyPVYL5CmtSXVBvqdUX7BuaC559s9K5CfE4HaJpdB6g9qXt4AHt1BW wViWOixqTSBIDI0hDzdJLP/8rcPL7koBPpNPgRkQAh4H3+SJ8z3YTsfWf9BqHGzzJd4a xGBZ3glfZx7wM1IA9Xy+qLzHw6ofO9QE8Fx0hWgacgPgVVMsbAxIvlKTQpLypKy+cad+ UNYg== 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=tIkw7Yhz1fDobLruZQ9dGfevX+0YNoWbemi0+agaonw=; b=s5V9Chd11eK015HS6RU00ZR/k8vqypdqlp3FTB9hg4MbJMFcZ/2gLZDIZ4MnMxnHek p8OXLILygcqIVWl81pd6A7p00hDAPaG1USHU9oG5nBK19Ku7SV0vGTH8WlNlS92wgR9o otHUtKosv21QXJQ1J3uRS2UdHLQyiUxjvw7py7364Hkw42/jBHjLbnwEkUB3i+98rSU7 LOpZF1betzxu2eSB3gYZ1+wY5zHoLS6qv8UU+xjI0wDSgQQAjUOtXdrX8CHbzn2yigY8 0SW8L47SLxG/x4EM1hE9oEejq0sNxn7piRIRdXRxLnSRX5ikICu2NEu793ylar6z3SVC UuiQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gLSGThtQYMr/x6c1TLhZxnW3whJ7dJCDSme5/YBytY2pz7S1uoa j8isOdzyGPZrlbw+uAVs8tw= X-Google-Smtp-Source: AJdET5dUFqACdinXIpJrHVnS3ubBCx2h6IPmawJdlfuUKwLSMQAxQLLcixCE8mKUsC41cTbVoFqKNA== X-Received: by 2002:a9d:43:: with SMTP id 61mr30915ota.3.1541591013524; Wed, 07 Nov 2018 03:43:33 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5e04:: with SMTP id s4-v6ls940699oib.4.gmail; Wed, 07 Nov 2018 03:43:33 -0800 (PST) X-Received: by 2002:aca:4892:: with SMTP id v140-v6mr37169oia.1.1541591012923; Wed, 07 Nov 2018 03:43:32 -0800 (PST) Date: Wed, 7 Nov 2018 03:43:32 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> In-Reply-To: References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2859_1289561053.1541591012250" 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_2859_1289561053.1541591012250 Content-Type: multipart/alternative; boundary="----=_Part_2860_93201536.1541591012251" ------=_Part_2860_93201536.1541591012251 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 category= =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 Lumsdaine= =20 wrote: > > Ulrik=E2=80=99s email nicely lays out the three key notions (pre-category= , 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 use= =20 > =E2=80=9Ccategory=E2=80=9D for a definition which doesn=E2=80=99t come ou= t 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 differenc= e=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 for= malise something=20 > using =E2=80=9Ccategory =E2=80=9D to mean =E2=80=9Cprecategory=E2=80=9D i= n 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 a= n=20 > innocuous one; it changes the character of the resulting =E2=80=9Ccategor= y theory=E2=80=9D=20 > in interesting ways. Making the restriction to univalent categories taci= t=20 > is misleading to readers who aren=E2=80=99t fully =E2=80=9Cinsiders=E2=80= =9D, and obscures=20 > 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_2860_93201536.1541591012251 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I'm a bit confused by your message, Peter: HoTT doesn&= #39;t have a naive set interpretation and is inconsistent with UIP, so I= 9;m not sure how that should guide us. (Maybe if we're working in good = old (agnostic?) MLTT?)

As I tried to say, I find that pr= ecategory is the novel concept, and that both strict category and univalent= category should be familiar to category theorists. (They have a mental mod= el for when one notion is called for or the other, but we can make the dist= inction 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 th= e three key notions (pre-category, strict category, univalent category), an= d the argument for the Ahrens=E2=80=93Kapulkin=E2=80=93Shulman / HoTT book = terminology, with =E2=80=9Ccategory=E2=80=9D meaning =E2=80=9Cunivalent cat= egory=E2=80=9D by default.

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

Based on that c= riterion, 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 usi= ng =E2=80=9Ccategory =E2=80=9D to mean =E2=80=9Cprecategory=E2=80=9D in typ= e theory without assuming UA, then you can read the result either as valid = in HoTT, or (under the set-interpretation) as ordinary arguments in classic= al category theory, with all the terms meaning just what they traditionally= would.

Univalence of categories is an important a= nd powerful property, but not an innocuous one; it changes the character of= the resulting =E2=80=9Ccategory theory=E2=80=9D in interesting ways.=C2=A0= Making the restriction to univalent categories tacit is misleading to read= ers who aren=E2=80=99t fully =E2=80=9Cinsiders=E2=80=9D, and obscures under= standing its effects.

=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.
------=_Part_2860_93201536.1541591012251-- ------=_Part_2859_1289561053.1541591012250--