From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDN3H5PUGYIMDZUL34CRUBBYQC6YK@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 571ec1c5 for ; Wed, 7 Nov 2018 14:14:26 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id x30sf10788815ota.7 for ; Wed, 07 Nov 2018 06:14:26 -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=SpJfd7ti3tRQvh8GtneL+rvog38luKRsGrkGYHlrQMA=; b=g3lfASAkn6s/FKXLKFKRG1Caja8F8dsHWm8tnSGLS4oJmU5FgpkGhpuqyhg3LEGfZ1 QcOhkxwsU4MetyLhDYvn95GKKgi2lTAhSQEm3x+mGwQM/Wfu9iiEjJ3/M+Tb1JoVZIjQ m2dv65UDS8F99F5eTCdW4OCYL18vDTXoZjYzXccOHCOJx9w6ZaeWPL7QWNFjuGuaZxV2 ShZpJFRbNEicbJxglosJ36scs2T3mUjD0gyzHMwV8WmKr+3MqbrCFsDLhSHqTVG4FnSk zLGBn5Wf9BFJcl6kagGRJBTjDPZQBGAn9t+3JSkDWVzj5dz9cO4wMFcXoLHsdcGoG660 Uv9w== 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=SpJfd7ti3tRQvh8GtneL+rvog38luKRsGrkGYHlrQMA=; b=lifdttOJRGbNPd0A0eLpSOqvU50tzgXwWCxQHXWZyNVVMJHdA9TM5WEeMHHG2nmK9A 74ty4Y7JkUrO4mSeZH9xs9uCRK4TzzKKGkQ3HhL/2VDkVL2KFa0n12iG1mBt/avtQypY 74Gdjm6pa1wbQNCIohQo0V9VProwc2nt29ue1ZMb2ZBPcwebdqcvq+Cfjk0qjdTGtVV1 tchSJxBytopGQBb9bkT+MYaOD+VcU6wCedUU+CgePfQKDv6SMkNYOWqFF723jl64L0uB lkYU0r6L9y8Kd2A8o6vtJhIbS1BJlmTRhFR8h5TXHWMylO3PzhWGjEVgrV/gQrIyCG3j RJVg== 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=SpJfd7ti3tRQvh8GtneL+rvog38luKRsGrkGYHlrQMA=; b=qKniV47OdQuPZo5W9hzWqRj21JizqcY6INM/OEeeyEJnM/z3rIiw3NRfX6K6XLS+oc DumDzeQf9L7Z5/IUD9EGtzh01PUjdtP2VJGht4gMHudPXKJe8DMr9/wu8oWvAhe+Htz3 xkq/tyzJ+Kc6SozCSTZJRmSL/QecRVZ1QCyraTAkugvm/TMvAPNItBtbY/d/Bn1xfLLY lcNzFmK//wjK/6fRTkmov6OI8oE43BOS8VGKSpCL8Q/m2cuMiKjdzxVHPrq+zCH0nKhg MBL/XY9LrBrFya8HsDYQz7Qc3vzu0FKr9ph9YpwJnrO2Tf/M73Bo/Nl2+CX5zh5AT+Do jY+A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKDc67gENJgGqQqj9aln9mjvARl90vvA2Ocm7OVvTgYisM9+pZ4 MZrPuHS9IsE1mXprdffL2fI= X-Google-Smtp-Source: AJdET5ewqPng101quoMJ3wua3jXjGXA/l2kYckQGt5lEc1bU/G/YfOmuRcgGphHycL+GnC2x05nVXg== X-Received: by 2002:a9d:5e97:: with SMTP id f23mr5807otl.4.1541600065410; Wed, 07 Nov 2018 06:14:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:ecc:: with SMTP id 70ls5039707otj.1.gmail; Wed, 07 Nov 2018 06:14:25 -0800 (PST) X-Received: by 2002:a9d:43:: with SMTP id 61mr5725ota.3.1541600064867; Wed, 07 Nov 2018 06:14:24 -0800 (PST) Date: Wed, 7 Nov 2018 06:14:24 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: 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_2933_11890265.1541600064340" 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_2933_11890265.1541600064340 Content-Type: multipart/alternative; boundary="----=_Part_2934_666907564.1541600064340" ------=_Part_2934_666907564.1541600064340 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorsten Altenkirch=20 wrote: > > 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.) > > > This is too clever! > > =20 > > If you just transcribe the traditional definition of a category in type= =20 > theory you end up with what in the HoTT book is called precategory. This = is=20 > confusing for the non-expert even though you can justify why it should be= =20 > so. > No, you get the notion of a strict category, which in some sense is all=20 that you directly have in set theory. (To get the (2,1)-category of=20 univalent categories, you take the homotopy (2,1)-category of the folk=20 model structure on the category(?!) of strict categories.) As I said before, the notion of strict category is useful, and encompasses= =20 the examples that Erik was missing from univalent categories. But from a HoTT/UF point of view, the notion of strict category has the=20 drawback that you cannot get a strict category of sets (or groups or=E2=80= =A6)=20 without assuming the axiom (a homotopical taboo) that sets cover. --=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_2934_666907564.1541600064340 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Wednesday, November 7, 2018 at 2:58:28 PM UTC+1, Thorst= en Altenkirch wrote:

As I tried to say, I fi= nd that precategory is the novel concept, and that both strict category and= univalent category should be familiar 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!

=C2=A0

If you just transcribe the traditional definit= ion of a category in type theory you end up with what in the HoTT book is c= alled precategory. This is confusing for the non-expert even though you can justify why it should be so.


<= /div>
No, you get the notion of a strict category, which in some sense = is all that you directly have in set theory. (To get the (2,1)-category of = univalent categories, you take the homotopy (2,1)-category of the folk mode= l structure on the category(?!) of strict categories.)

=
As I said before, the notion of strict category is useful, and encompa= sses the examples that Erik was missing from univalent categories.

But from a HoTT/UF point of view, the notion of strict cat= egory has the drawback that you cannot get a strict category of sets (or gr= oups or=E2=80=A6) without assuming the axiom (a homotopical taboo) that set= s cover.

--
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_2934_666907564.1541600064340-- ------=_Part_2933_11890265.1541600064340--