From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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-oi1-x23c.google.com (mail-oi1-x23c.google.com [IPv6:2607:f8b0:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 9d17da0d for ; Thu, 8 Nov 2018 21:35:56 +0000 (UTC) Received: by mail-oi1-x23c.google.com with SMTP id y81-v6sf13724676oig.20 for ; Thu, 08 Nov 2018 13:35:56 -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=qZV4KHa1sWycdPdrlopVuZ2ogpCyYlmdGPwX6XzFPAw=; b=koDcglfuSwh3Fwop6GuoOX8h5rTjzHTR8TSzrngpEqNWXrRkyi6tN2TOBeVaexhMld 2dkwzs7LrCKP81VmYvd7fLu1zd2eISdm3KYjY3zwXrrHowkHBCb8WfqaQdlOC3JGM/WL 9MqztPBmsMkw/2FsbRNkF1Gu03aDO1NstUfDjgFok6EXJ5MMTcpf9reX0qPO+X7Gt/2S buZz5c2/y/2J/Ptht0B+ANxV9TkkNdwITtTs4dwye/P7cWs3paAoYub5Jk56kWuRfiQj QjhUjapYMkHjmmGGo2/LTVNI/wyL3S01JIKfx7NiHv9KT3IQcOqbWpgziWbl0fVEcmGO h65w== 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=qZV4KHa1sWycdPdrlopVuZ2ogpCyYlmdGPwX6XzFPAw=; b=YPd442266+W6FINm4QFJByMeyqAxMjj3NY8n6t9hzky7psomkGJOzWIcEpKn5zxsEw XzgWc008Kt5ZzVQfFISDMVf8UkPA/+7VTEJiQHlvo4EX0C3TVqZwRKhHilXbO/5vpI/Z MX9tbygDb5EO6Vr33UAzbIyejb9Qj7EeiQ4g0cK5hHlRNIQDKEk5fbYF8F0b5q7V21vT nmgSKnVdGDV1gKWB4FN5X3h5oV2f+rHFHMi694eRx4mwOygeJy2kU7kBApV963nFDG3H sN5yJh+VIAq6hw/6ImTV/g+MMnXgL3X5RkTabfQw9ya/HyHpj18gAiQzI5zDEMh1hzUS 74pg== 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=qZV4KHa1sWycdPdrlopVuZ2ogpCyYlmdGPwX6XzFPAw=; b=mGMv02tQN+MkJVP8VeZ0R95hCDMybMX8yUdnL641ILIj/17+VdbnZrcRmSDgt4hecn P17etPgMS5M6cJazKuJr1vMGB019GFkHueDARGFi1XyH47wbPSp9mlYogqV8IvVaq9Ic aR08t4CWLct3ujLWf0M1D/Zp3ZSiEsEQktntObv4qKJRWZaWdhtc3hAedghurUp7B+XJ 2AVLlE1mlv3mcFJM3SkXGnGRg44REC7b007qbjMGnpSq+OEAGfUWkjhqCELQUup46aMa 4VOQsx6d5DRrSG+6g7MX7fI/cQSEMqygY/RE9fqGOjYKUcf/dAhnYQbNuQQ8syH9ELOO L/Wg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKFxvBpq+WFopADP9uGXDi3pAQ0/nKsa2u+YTC1y68QfI2TZ69P Ret7Lr4x9qt4/AWc8OXlj+s= X-Google-Smtp-Source: AJdET5cSAcja4xW3i1nWq7jouxuSkcineXgSw64r6hNHp1VNa80BEqIrxu+b//6LUKAifxEhxJuDJA== X-Received: by 2002:a9d:5403:: with SMTP id j3mr104692oth.2.1541712955673; Thu, 08 Nov 2018 13:35:55 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3016:: with SMTP id w22-v6ls1476000oiw.3.gmail; Thu, 08 Nov 2018 13:35:55 -0800 (PST) X-Received: by 2002:aca:889:: with SMTP id 131-v6mr61160oii.3.1541712955069; Thu, 08 Nov 2018 13:35:55 -0800 (PST) Date: Thu, 8 Nov 2018 13:35:54 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <9a48ae27-6a8e-4bfc-84e5-1ba4de66ca88@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_734_1391532662.1541712954378" X-Original-Sender: escardo.martin@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_734_1391532662.1541712954378 Content-Type: multipart/alternative; boundary="----=_Part_735_165955222.1541712954378" ------=_Part_735_165955222.1541712954378 Content-Type: text/plain; charset="UTF-8" On Wednesday, 7 November 2018 10:03:17 UTC, Ali Caglayan wrote: > > I want to get a general idea of 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 being 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 precategory 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 "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_735_165955222.1541712954378 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Wednesday, 7 November 2018 10:03:17 UTC, Ali Ca= glayan wrote:
I want to get a general idea of peoples opinions when it comes to naming c= ategories internal to HoTT.

On the one hand I have seen,= in the HoTT book for example, precategory and category being used where th= e latter has the map idtoiso being an equivalence.

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

Now because we have = Rezk completion every precategory 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_735_165955222.1541712954378-- ------=_Part_734_1391532662.1541712954378--