From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCR53C7ITYGRBEUQRPPQKGQEA6M6F6Y@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-ed1-x540.google.com (mail-ed1-x540.google.com [IPv6:2a00:1450:4864:20::540]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a086eb27 for ; Wed, 7 Nov 2018 11:10:11 +0000 (UTC) Received: by mail-ed1-x540.google.com with SMTP id h25-v6sf9290528eds.21 for ; Wed, 07 Nov 2018 03:10:11 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541589010; cv=pass; d=google.com; s=arc-20160816; b=EeZbp0KlYX2Whono63UPrWRiJMqCr2VcTzvioGyQA0uwgBZxj5o02tr/ReZO7jvBOU ZfbzROzOC2HqdC/RhNBwrEpmoHQoceyYjZwxgiGePurZ89xCvcsbeRSIFCaY2AqDAZhW RT7446tjCw4JTs7k2tpDcgcJ/ZH+4Q5shPX5ACNahr/IGJco65fXeegyzES/GTl1a2BU 7X0QRBemfn0XwjMypey7y/qipU55usOlSd6wlh3Z9IWRDDA8bzYaaApd3A5UOlHEYAM4 qm7gn3XbCTU+uTSYSRVqRCyYaEGrl8wGVcVMBCGFSxl5VqmEfkNUUm4fdwKgh6ENUejH 9FTA== 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=R2dIBlSZldj2roC1X3ftPR9K2ATXiobUkCPDpAo9hMk=; b=wtclGRoKkGseb1ylTZ55HtW8FMd7FAuktJIZnyeHQSmeta6rymT8QNpZppj01DrXZL nf6G8wIGTXrbMSkxDjKFDJKwQLMeTtoT4y1gGVtqos4HqVLyd6clNr1kFFTaxHF9PNkC gtySHnaL6Y0GbjqTlKJaqgbGFdlr1q0XaVeJu+zWfi8s4wHplaowFjX/xk+JSTygO1KW XLNDzRf/aS9xMZ/Yr1rOze2GmOzuVRlemngDDDJj4coZhR2FDelaJu6J8x/oZPtVF9wB UkvCJJKQYhx/716TX5gt3Q5vFBk/QtHEjSCWSOT5Ly9Ozf1hcKOqByFWBzxO4R1HtRbz mtPw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=kD4iy6t9; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::531 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=R2dIBlSZldj2roC1X3ftPR9K2ATXiobUkCPDpAo9hMk=; b=DMRB8R5q3w9B7GIPcsxe70t7lQhmRpjic+G2GA90pm3BKT9GIMrljfDMTMo7K4Mu4D v2PK3lXS/lw8+HAXeEu+t5aiPeowI4ZtpFSF38nn41Y8lJaAmueWrvCcIH+Du4fEGxJ2 NSf8sZlKgY0hW3Dl0EyujI4moJzpq2NwQla19UN+OoXmYDYdbefydGFzsylIMU+JxY7P yqVmKqamwMXIjbXgF+KrQY4R7kcUIyNqYCeLj6Ji9I6RRH36hkO++gTY6oaE7AeIbRac qeCW0HfPfcjVO3NOWY7jGropmkK5uMvBqOsaHsFh7j+l8g2KqAyLH2VhYYQi5WJRVaDw yMjg== 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=R2dIBlSZldj2roC1X3ftPR9K2ATXiobUkCPDpAo9hMk=; b=uP/YV0zDmR1uDpdcp+KTOyfYtBC8MzKjak5a6bqRAiRIyU2iZhP4YOMiCKEFipxs4X UiZ0JRqVQVl5rZRk7fml1clmdjPfS4AckjJr2B6YlhBW9uiAlwuqYntJHW2EeykInB97 BVgmZJCThVprDl6UbQLmnLqqdj4tH9b5cz0HNszR606M4FdC0va3PVSG8VCAKJ2H5uaT DKX+A/nZjF+aNx9zQ7GbVeI26zWIS1/LOWGKHWdhBFmhYcuQZyBENZHtItS/6Vd7Kj3g z0LkKqNG1sdG4CHauWcMCQ9WWAaW9FqkImVr3ujZiKK6SpN3v6t8gaduQjp1lhSPeDYR 4/dQ== 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=R2dIBlSZldj2roC1X3ftPR9K2ATXiobUkCPDpAo9hMk=; b=BzGpHO+0zssGzH4gV7gXDsPXFuTJavWRmU4MT+JKrjgtqYoc0Yrr80WmdfTj3gZT3d XmI4m5qdMfOUhS2eW1UDcv5vUBF8dc+5csHD9E30yQACsYSVRFj53dMvIVb7RJZDx6pc mhe1kqYMbGUOuh2GRfVcmq481ARS2ai5EpOGCAbz+7gpVfO6mVv3sHV+ETWX7nnKAwrU R1+tqtiSrhX8dzZKY0L3orRG649nLB0CfET6whvOpz+6lJL+B6n0qa6yYRf0ngmJD0ch 8bpLj7NmprZ943N/AtSyqxFr89gT+h5C6gl/4a0/AJ047yzykxOs4FhM0ObdZ1VC63F6 gF4g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKDwzEz6AeTl6/8S/fEzjawiru/6StSLUOl99XjFKdeiHNIb0wW zQOXTyY7n2OwKAa0rlYEieI= X-Google-Smtp-Source: AJdET5f+egPkzAq/MinSm/d2OJfCPPzuxL5l4NEbISwEBAssO8bfAJTOwEdQL1sPDkgFo0MK2poJbw== X-Received: by 2002:a50:893b:: with SMTP id e56-v6mr8047ede.3.1541589010529; Wed, 07 Nov 2018 03:10:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:3017:: with SMTP id 23-v6ls4985171ejz.13.gmail; Wed, 07 Nov 2018 03:10:10 -0800 (PST) X-Received: by 2002:a17:906:328b:: with SMTP id 11-v6mr287013ejw.14.1541589009977; Wed, 07 Nov 2018 03:10:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541589009; cv=none; d=google.com; s=arc-20160816; b=jNnuVw5UJKnPft0ZPeApEbmMiy56bpjkMZdxJx/STikfTlIV65asgf2B8N2J/I0IGB gmYEzx2O4Po+/zwwBJKVyHq5xZDrmihL+xRNY8pYDheFhWkcRuRIu4tfayr8q//FSdou KxP447N/xGIZTo7yv6n0bqdJocdvNfxlv/JbTDinZHhH4JZCIunTgu035wteksLchavQ IpdQMogutrotG6cJGq8mO+jm4W0HNEHY3pJP/N3OCKAvtESF7rqZci727wTiXOFbWOKS z8rQqRQF5bOgLDKe4Pj2a5GG9CrXfdBB7d+4H+myLbi689gPy0E6KPC7ttn4tTqk5gjJ QUIg== 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=YIIsbGvzQoIbomSdE1CksxOt8ZnA4e8lM8ZfBYA1HsA=; b=zo46NvYQrx6LfYIUUgrvJ1x1b+o+ZXk2hRh9Q1uAt7x6TaGQvv+N21ZE4JIbXK7so1 TcxPv+sxTUuC1PJ54bHqW8p8N+9aHNDSupqRYO7fFy/N5IwJagD75rmUn9kupVLcN7yn VDA5xzqDi6fYO5aTlbETK6ExurJxitowgz2SbN2E8NWeT5YpH7NVAk+U/t+bAhQKR4MR AjXczn8Efw80JERAB2+vpYSkiQB052SBA+SPTGhCILeFnSq+1l2umdMxARFArrsFneNu yvu9hQaAboa14ZK+UQGTmyWTX7o6Ijit4iDTevVi/TVTfJja3qJH1Dj51ed24PwuLBqB BG8A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=kD4iy6t9; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::531 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-x531.google.com (mail-ed1-x531.google.com. [2a00:1450:4864:20::531]) by gmr-mx.google.com with ESMTPS id n20-v6si16018edt.3.2018.11.07.03.10.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Nov 2018 03:10:09 -0800 (PST) Received-SPF: pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::531 as permitted sender) client-ip=2a00:1450:4864:20::531; Received: by mail-ed1-x531.google.com with SMTP id n19-v6so13051788edq.11 for ; Wed, 07 Nov 2018 03:10:09 -0800 (PST) X-Received: by 2002:a05:6402:7d4:: with SMTP id u20mr1786691edy.81.1541589009681; Wed, 07 Nov 2018 03:10:09 -0800 (PST) MIME-Version: 1.0 References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> In-Reply-To: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> From: Peter LeFanu Lumsdaine Date: Wed, 7 Nov 2018 12:09:58 +0100 Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Ulrik Buchholtz Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000004fd315057a1129e0" 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=kD4iy6t9; spf=pass (google.com: domain of p.l.lumsdaine@gmail.com designates 2a00:1450:4864:20::531 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: , --0000000000004fd315057a1129e0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Ulrik=E2=80=99s email nicely lays out the three key notions (pre-category, = strict category, univalent category), and 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 category=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 th= e addition of UIP to the type theory). 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 makes to the development of topics. Based on that criterion, I strongly prefer taking category to mean =E2=80=9Cprecategory=E2=80=9D. A big payoff from this is that if you forma= lise 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 category theory, with all the terms meaning just what they traditionally would. Univalence of categories is an important and powerful property, but not an innocuous one; it changes the character of the resulting =E2=80=9Ccategory = theory=E2=80=9D in interesting ways. Making the restriction to univalent categories tacit is misleading to readers who aren=E2=80=99t fully =E2=80=9Cinsiders=E2=80= =9D, and 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. --0000000000004fd315057a1129e0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Ulrik=E2=80=99s email nicely lays out the three key notion= s (pre-category, strict category, univalent category), and 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 category=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 whic= h doesn=E2=80=99t come out equivalent to the traditional definition under t= he na=C3=AFve set interpretation (or under the addition of 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 c= lassical analogues, and see what difference HoTT really makes to the develo= pment of topics.

Based on that criterion, I strong= ly prefer taking category to mean =E2=80=9Cprecategory=E2=80=9D.=C2=A0 A bi= g payoff from this is that if you formalise something using =E2=80=9Ccatego= ry =E2=80=9D to mean =E2=80=9Cprecategory=E2=80=9D in type theory without a= ssuming UA, then you can read the result either as valid in HoTT, or (under= the set-interpretation) as ordinary arguments in classical category theory= , with all the terms meaning just what they traditionally would.
=
Univalence of categories is an important and powerful proper= ty, 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 restri= ction to univalent categories tacit is misleading to readers who aren=E2=80= =99t fully =E2=80=9Cinsiders=E2=80=9D, and obscures understanding its effec= ts.

=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.
--0000000000004fd315057a1129e0--