From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBZXQRLPQKGQEGQDSN3A@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-oi1-x23c.google.com (mail-oi1-x23c.google.com [IPv6:2607:f8b0:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2175bc00 for ; Wed, 7 Nov 2018 10:03:20 +0000 (UTC) Received: by mail-oi1-x23c.google.com with SMTP id w131-v6sf10537811oie.4 for ; Wed, 07 Nov 2018 02:03:20 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=acqocwietJtEVDffT6XPUzuekrvnFQXx9z4hIstzPvo=; b=SGf4/LYHKVrWPyoUScSslEkntERioRBKB5lhAPxPGWtslUSyTvCLlRYt9bSIkRSIz9 MzXEaKZKzle+wNXH3a/L8Ds7tHcshBODEj66pCDRt9/E1xZBEOfGX/Zkw9J+7EHnpe7E l8pS+KdZomRK8JezudTdeAmiQhRiwnlfsMWhVdB9eCkdFf2yw8Ep4vhJUIPu8wXCxKX5 blkmOHSXkoKzH9zt4Bquc22G5tosf4VpZEJW4eZwZImAyasXR7Ixiv7mU+w52ussHBno F8/6oA/sOLwlDo0QbxkOlVvDwmTXEy9GEBC/TeebDjMHdOrxmQBn0ck1ma3oBcsf8qGL 8Agw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=acqocwietJtEVDffT6XPUzuekrvnFQXx9z4hIstzPvo=; b=MoEEDsNUkPRKZB641jjLX7jDnb4W7OrOj+UzA8DcdD/qfp3PhD6NRFaA4oEyFEGuvv S6IqkLqLaueM3nA+lPdERN2J5IAzTT2C+IDMwVis6A2iLqv8L1ZkU+FysJ6Me1afxd7B NwD7q71bKojdGb/IsQr9/GfrwvM5mLxWVV25NkrEUZTQtFwb/WyQv/GB9yuJ1oJBzPrv MGfxnjp4meI8FgVp+9DBbHNFfBHDiHBvND/Zek0JcvzbCtxRqszjgeSpt0mOnFzsJ+f3 +UwnAPn9F7kM4qCsNfUkxriSBLeHUeAmWAv2fmKQ6njDC93zz5H2HdK1Y/ksKsFaq6Hd Ra7Q== 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: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=acqocwietJtEVDffT6XPUzuekrvnFQXx9z4hIstzPvo=; b=SYv60JRbCMVX5Mjt0zUshhJCgBETGLkggQMyiCJY5MqnN/N4Wj7IZYkTcYsyZ1EREP j6h5Vq1UDgKWVmRf2AC/QGRn4CNnDcby61qGvjZYM6Q6M8XekWUZcuMyMmawGagPPJfI L9STnZXMTNxgENqQIaI5HoeIfSsHMpOvR4/Q5vokH9DVIvXm4PI8q6jyIOg59xIWFcSP hXLYbusnHmXL113txpt8j1Op+BfQIEPjAeDjyy4sosXiOupEWsd/9hdj/sjf9pj8y5za WkWRdpKu4Gt5AmtAfWspg/vvvflqVvoOS4PIGP27ntytqNf9bkcYi1wtRl7DZvT8V3Xv CTXg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gKP+jpXjKo7rMogxNhuFkj5BUr0dGtatjg/F4dI0/peJhpQuPo6 IZaXoQ7qad6oM2xv8++tsks= X-Google-Smtp-Source: AJdET5cgIvBIbph0qd6oeTyQUJNsEDZBbdPK7JYD7tLRe3FXuPRKN2KF9aFwU/Osg0ZZjF5smk7jBg== X-Received: by 2002:a9d:bd5:: with SMTP id 79mr25320oth.7.1541584998944; Wed, 07 Nov 2018 02:03:18 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:bea:: with SMTP id 97ls381520oth.8.gmail; Wed, 07 Nov 2018 02:03:18 -0800 (PST) X-Received: by 2002:a9d:5e97:: with SMTP id f23mr26446otl.4.1541584998348; Wed, 07 Nov 2018 02:03:18 -0800 (PST) Date: Wed, 7 Nov 2018 02:03:17 -0800 (PST) From: Ali Caglayan To: Homotopy Type Theory Message-Id: Subject: [HoTT] Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2454_533508041.1541584997813" X-Original-Sender: alizter@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_2454_533508041.1541584997813 Content-Type: multipart/alternative; boundary="----=_Part_2455_1184227820.1541584997813" ------=_Part_2455_1184227820.1541584997813 Content-Type: text/plain; charset="UTF-8" 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_2455_1184227820.1541584997813 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I want to get a general idea of peoples opinions when it c= omes to naming categories internal to HoTT.

On the one h= and I have seen, in the HoTT book for example, precategory and category bei= ng 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 c= ategory, so some might argue that a distinction isn't necessery. I woul= d argue that the HoTT book convention is infact more misleading as "pr= ecategory" there is really just the usual notion of category. And a un= ivalent category is some nice structure we can add to it because we are wor= king 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_2455_1184227820.1541584997813-- ------=_Part_2454_533508041.1541584997813--