From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDN3H5PUGYIPFAEL34CRUBBF47LWO@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-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f43dd7ca for ; Wed, 7 Nov 2018 10:37:39 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id 30sf10666926ota.15 for ; Wed, 07 Nov 2018 02:37:39 -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=Lz2CYFir8hRaNYzSl5HbAaZzQoWTP3/gSxRL3QmIW7o=; b=qOclk6Z8SMm9RfliU3TKjrLKOtiYkz+yKL+nk+MukrdwKBl8N7jhaxmkAtHrI3caQ1 rlP4Rwbqw+IrUuR1JYm3FFILf2B85W8CRInAIdYeC/BT6HRui44WOgZ3ebnVLK75YFnT swrVuLiNS5SMy/wSLxWzsC3hR6KLQ5E9r8QHzQcW3n4dKPaq+vjuA1x1V+xwf61T/P7p bbl3zS//LqcLOKiV3UiVghVU7rcobU9D6O1I5IzBvfa4WC3UHAex4E0Sxmfb6lY5QzBH Hfw1o7Q3VXt1bOe61eaAzo+iQJ66NAyzKNN9CdrS8q/BdK0SiDBYigYWYse5jQ1N8Bj2 bYbQ== 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=Lz2CYFir8hRaNYzSl5HbAaZzQoWTP3/gSxRL3QmIW7o=; b=fZCF8Nbw7cFJTar88or3s7hjbMxU6I1pE+nGA/b6wqQCY5pR82tTJrs9MesW6YtwRW hguAtm06j+xY3ww8KwzQlenv4MEXWtFjtqSU90FAIrw7b4y2K9/IglnwPOoSR/2yZ033 y7PHbC99P36ZySNYA7nGkwMu9RAt9n92Z67dy57JCHGApBJtvwd6Vk1R4Rd52FSwrjPp tmUtl4kqZxL7yxzFVWf3NbAL5ISzWH4aPORWm7N8GndBcl4riWbFf2BKWamQLzP6ULR9 45Nd74DXq3IohUZn+53+zQiRDl9YNhUdf9i0d1BS1k0VclhtGu3EZOVde2kevj4fc7PE bbjA== 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=Lz2CYFir8hRaNYzSl5HbAaZzQoWTP3/gSxRL3QmIW7o=; b=SaN5IufYgTNxkPiO59BY9dGcTjPX4IEvgfB7JMBRvy71fnkJNI47aMlubFF1ArEw9E 51ZeY69DXEZlOX6O2vP7PlLSfBAuW3ChVrxbXRALK3say2iumx4SDqtorYhwUnX81xwl KTsxFEiprtP2k/RUjfpWxVhLXlbmXc9EubGzj67fL9rgNV93y0EqQC1URws4+oWRQMYL hdDhSm0UTvdAT3PL89UbMnGlAiK1+6oW4bxveYDJZ91TCf60JlkCUAtrfMIwagmzGv0Y Lp8Y6pqlS5nsev10nUTX0o0grI2+i2Z/RXabaHG70LwUjmBzoSyiILq0QKLDyVqUFZBx BD2w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gL0EUqbXknRwCNFK87CFmDStiyh43ZeWvxPh2oWfx1tWZucWMrU PPFtQHgh90jqkUhw4kboxSc= X-Google-Smtp-Source: AJdET5eqNRrydEQRaRvVZDjVikp0U79KJd6zZ6oSukGOeo0tw7EdI6zYVIbpJKsabv6oXxsUo9e9cQ== X-Received: by 2002:aca:56d0:: with SMTP id k199-v6mr30456oib.0.1541587058923; Wed, 07 Nov 2018 02:37:38 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:bfc3:: with SMTP id p186-v6ls867598oif.6.gmail; Wed, 07 Nov 2018 02:37:38 -0800 (PST) X-Received: by 2002:aca:a984:: with SMTP id s126-v6mr31335oie.6.1541587058593; Wed, 07 Nov 2018 02:37:38 -0800 (PST) Date: Wed, 7 Nov 2018 02:37:38 -0800 (PST) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: In-Reply-To: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> Subject: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2532_1049494386.1541587058098" 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_2532_1049494386.1541587058098 Content-Type: multipart/alternative; boundary="----=_Part_2533_97166764.1541587058098" ------=_Part_2533_97166764.1541587058098 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mine and Paolo's replies crossed, but of course I missed the condition that= =20 the function be surjective. On Wednesday, November 7, 2018 at 11:35:11 AM UTC+1, Ulrik Buchholtz wrote: > > Hi, > > First, there are (at least) three mathematically important and useful=20 > types: precategories, strict (or set) categories (precategories with a se= t=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 categorie= s=20 > (categories together with a type O and a function from O to the objects o= f=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 usefu= l=20 > concept. > > I personally prefer to keep =E2=80=9Ccategory=E2=80=9D for univalent prec= ategory, 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 n= ew=20 > concept to HoTT/UF. (Although infinity-groupoid flagged=20 > (infinity,1)-categories arose independently in homotopy theory; these cou= ld=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= =20 >> and 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 necesser= y.=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 ar= e=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_2533_97166764.1541587058098 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Mine and Paolo's replies crossed, but of course I miss= ed the condition that the function be surjective.

On Wednesday, Nove= mber 7, 2018 at 11:35:11 AM UTC+1, Ulrik Buchholtz wrote:
Hi,

First, there are (a= t least) three mathematically important and useful types: precategories, st= rict (or set) categories (precategories with a set of objects), and (unival= ent) categories.

I take as one main lesson from HoTT/UF = that mathematical objects have types, and that the identity types should in= dicate the relevant notion of identity.

The t= ype of precategories is equivalent to that of type-flagged categories (cate= gories together with a type O and a function from O to the objects of the c= ategory). (The equivalence is given by pulling back the category structure = to get a precategory structure with O as the type of objects in one way, an= d taking the Rezk completion together with the object part of unit map in t= he other.)

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

Two stric= t categories are identified via an isomorphism, and two (univalent) categor= ies are identified via an equivalence.

So I disagr= ee that "precategory" 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 univalent precategory, as most often constructions= on categories are meant to be well-defined up to equivalence of categories= . In the category theory literature written in a set-theory metatheory wher= e 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 point-of-view. The type of precategories as a c= ommon generalization of strict and univalent categories is, I think, a new = concept to HoTT/UF. (Although infinity-groupoid flagged (infinity,1)-catego= ries arose independently in homotopy theory; these could also be called (in= finity,1)-precategories.)

Cheers,
Ulrik<= /div>

On Wednesday, November 7, 2018 at 11:03:17 AM UTC+1, Ali Cagl= ayan wrote:
I want = to get a general idea of peoples opinions when it comes to naming categorie= s 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 being an equivalence.

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

Now because we have Rezk com= pletion every precategory is yearning to become a category, so some might a= rgue that a distinction isn't necessery. I would argue that the HoTT bo= ok 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_2533_97166764.1541587058098-- ------=_Part_2532_1049494386.1541587058098--