From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDN3H5PUGYIOB74K34CRUBCDUNMFO@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-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c76ca139 for ; Wed, 7 Nov 2018 10:35:13 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id m21sf10623507otl.14 for ; Wed, 07 Nov 2018 02:35:13 -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=CccHRT1tUPXJOeE/b+l2AZL6QTNAce4Xkd3PLtzsvgo=; b=qu9NGrcswCfXtGP67YEGJ8trqj4f+HaNxzLTXt3sMPqYDqeP4LmR0DdU9bMeKaqiMj zhO6Ha3UqlW3XNuYvGZeaTTxNkaRum321QZhWe+5msFNqeZGlnTnHQGCANpiHmKLxY9r pNYfv4p3K4w/19kSDLHDoDP4qkQBLk9l9q6MdBcIG1WwlgJreTTPWaMVEwwCcTxAD6wh ekmlH4wzyi1LJQqcnldE9FHfobYnPgwZCoO6eqsSCJidKddLgQq6cIqHt8z6/TQFYRyk 6mK0Rs2ZASmnnbDuoi6g4A/HceFKR9YxZdV01Q0J8c+jxjcxbGnL7KjN5ablX4obPNI/ GTwg== 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=CccHRT1tUPXJOeE/b+l2AZL6QTNAce4Xkd3PLtzsvgo=; b=EYH1aTg9aVxP4j1paHv29n/noi6HviyScmbSI9hykcwMkdwXI4IiNlQtksl2qqw8wl o2awQx5OotHhSDeTTi3sq6wLS5j76NBjadwBrBpk2qYKdNbloVtfWJIlwAGG5frocnty KeoaSPBU/1AcUfn53UzIM5zDWkz7Ss375pX0SBo4y8+gWal9FlhLe+9z7m1f0thAS5PM 4oJx1imBuf/9CJKU2IFGKdLKhseWgCGFLdv+8O+Tn++TbC5Vnj+YvCc5CmmpkR0OwZ2P 42UP2Qg+6JdrgezPjAv+0gRRHV7Y299o4FkEbaBFs+xi2hJdqTLW8rDnkNRkp0cHsB41 TK3Q== 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=CccHRT1tUPXJOeE/b+l2AZL6QTNAce4Xkd3PLtzsvgo=; b=qpfR0ccrhlATLJuusj+awL+6VUrlATF8Sp6qG8FbqGhCgCULui3ea6SVvhXrIQG1lE ODc3Agy7jAQftzwOHHZxBiNVH+2ScTRRjAQaObZeLTWwm7XOpxO4x4t9dZanIvPm9sr+ l2C+Gb+LjtM6YKmd1u2qPU9TDs+LO7uv/eAPOcTa48vvKM5Vkq9iBerAmQM/yE8/gQCT d9qExytL7xT/xQ4EJjB19cMkDme6EBiOXmo6C5JNhA9nAfiuhgjQOlVrEhwUEEmDPVyr KKZNipthGM9U6mkWcYGxcETPU3fEbhKj+rTJdD6epi9GtG6rAU/QL2jQDUWRKEkB7nGC vGfw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKn8vkZWOreH6FXbTuONDh4wSnLv0CzqXU/zfECkjQCfiPca3qs n+tLQgJ3JPdJ/kQqyTIw0y4= X-Google-Smtp-Source: AJdET5fFdHSDzTZjfDiZCPu3kJ5LDQwRZZzDirqRexJ/Qg82hcVH7u+gcfReoApvhTjsXSwWeQ7jMg== X-Received: by 2002:a9d:24c3:: with SMTP id z61mr27677ota.1.1541586912752; Wed, 07 Nov 2018 02:35:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3e8a:: with SMTP id l132-v6ls958106oia.7.gmail; Wed, 07 Nov 2018 02:35:12 -0800 (PST) X-Received: by 2002:aca:37c1:: with SMTP id e184-v6mr31574oia.5.1541586912008; Wed, 07 Nov 2018 02:35:12 -0800 (PST) Date: Wed, 7 Nov 2018 02:35:11 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2712_1979470377.1541586911497" 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_2712_1979470377.1541586911497 Content-Type: multipart/alternative; boundary="----=_Part_2713_1744789686.1541586911498" ------=_Part_2713_1744789686.1541586911498 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi, First, there are (at least) three mathematically important and useful=20 types: precategories, strict (or set) categories (precategories with a set= =20 of objects), and (univalent) categories. I take as one main lesson from HoTT/UF that mathematical objects have=20 types, and that the identity types should indicate the relevant notion of= =20 identity. The type of precategories is equivalent to that of type-flagged categories= =20 (categories together with a type O and a function from O to the objects of= =20 the category). (The equivalence is given by pulling back the category=20 structure to get a precategory structure with O as the type of objects in= =20 one way, and taking the Rezk completion together with the object part of=20 unit map in the other.) Two precategories are identified via an equivalence of the O-types and an= =20 equivalence of the categories, together with a witness that the square=20 commutes. Two strict categories are identified via an isomorphism, and two=20 (univalent) categories are identified via an equivalence. So I disagree that "precategory" is the usual notion of category: it can't= =20 be because the criterion of identity is different. But it's still a useful= =20 concept. I personally prefer to keep =E2=80=9Ccategory=E2=80=9D for univalent precat= egory, as most=20 often constructions on categories are meant to be well-defined up to=20 equivalence of categories. In the category theory literature written in a= =20 set-theory metatheory where the distinction is not so clear, you can of=20 course find plenty of uses of the word =E2=80=9Ccategory=E2=80=9D where =E2= =80=9Cstrict category=E2=80=9D=20 is meant from a HoTT/UF point-of-view. The type of precategories as a=20 common generalization of strict and univalent categories is, I think, a new= =20 concept to HoTT/UF. (Although infinity-groupoid flagged=20 (infinity,1)-categories arose independently in homotopy theory; these could= =20 also be called (infinity,1)-precategories.) Cheers, Ulrik On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote: > > I want to get a general idea of peoples opinions when it comes to naming= =20 > categories internal to HoTT. > > On the one hand I have seen, in the HoTT book for example, precategory an= d=20 > category being used where the latter has the map idtoiso being an=20 > equivalence. > > On the other hand I have seen people call these categories and univalent= =20 > categories which is also fine. > > Now because we have Rezk completion every precategory is yearning to=20 > become a category, so some might argue that a distinction isn't necessery= .=20 > I would argue that the HoTT book convention is infact more misleading as= =20 > "precategory" there is really just the usual notion of category. And a=20 > univalent category is some nice structure we can add to it because we are= =20 > working in HoTT. > > What are your thoughts and opinions on this? > --=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_2713_1744789686.1541586911498 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi,

First, there are (at least) three mathematicall= y important and useful types: precategories, strict (or set) categories (pr= ecategories with a set of objects), and (univalent) categories.

I take as one main lesson from HoTT/UF that mathematical objects ha= ve types, and that the identity types should indicate the relevant notion o= f identity.

The type of precategories is equi= valent to that of type-flagged categories (categories together with a type = O and a function from O to the objects of the category). (The equivalence i= s given by pulling back the category structure to get a precategory structu= re with O as the type of objects in one way, and taking the Rezk completion= together with the object part of unit map in the other.)

Two precategories are identified via an equivalence of the O-types = and an equivalence of the categories, together with a witness that the squa= re commutes.

Two strict categories are identified = via an isomorphism, and two (univalent) categories are identified via an eq= uivalence.

So I disagree that "precategory&qu= ot; is the usual notion of category: it can't be because the criterion = of identity is different. But it's still a useful concept.
I personally prefer to keep =E2=80=9Ccategory=E2=80=9D for uni= valent precategory, as most often constructions on categories are meant to = be well-defined up to equivalence of categories. In the category theory lit= erature written in a set-theory metatheory where the distinction is not so = clear, you can of course find plenty of uses of the word =E2=80=9Ccategory= =E2=80=9D where =E2=80=9Cstrict category=E2=80=9D is meant from a HoTT/UF p= oint-of-view. The type of precategories as a common generalization of stric= t and univalent categories is, I think, a new concept to HoTT/UF. (Although= infinity-groupoid flagged (infinity,1)-categories arose independently in h= omotopy theory; these could also be called (infinity,1)-precategories.)

Cheers,
Ulrik

On Wednesday, N= ovember 7, 2018 at 11:03:17 AM UTC+1, Ali Caglayan wrote:
I want to get a general idea o= f peoples opinions when it comes to naming categories internal to HoTT.
On the one hand I have seen, in the HoTT book for example, = precategory and category being used where the latter has the map idtoiso be= ing an equivalence.

On the other hand I have seen = people call these categories and univalent categories which is also fine.

Now because we have Rezk completion every precatego= ry is yearning to become a category, so some might argue that a distinction= isn't necessery. I would argue that the HoTT book convention is infact= more misleading as "precategory" there is really just the usual = notion of category. And a univalent category is some nice structure we can = add to it because we are working in HoTT.

What are= your thoughts and opinions on this?

--
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_2713_1744789686.1541586911498-- ------=_Part_2712_1979470377.1541586911497--