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-ot1-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id bad39431 for ; Fri, 9 Nov 2018 04:43:17 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id q6sf438462otk.4 for ; Thu, 08 Nov 2018 20:43:17 -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=o+zvoGVHiGiVgV9+hc2BfWC8Lhc+RYzq761m+eNgLEo=; b=MlYlk2Fl6JynxjNBRnNidjtg2ultzXfZUGAn0/tAT+Mljkp+pSFjBMYFZPFUBenwRo 9tZukIt1aHjYPKHWetFHBje3EcKu4RNlbH+LJHsEBE/20vui3cz6jlHy4ryQ4wgQ6zEb dlhl5bgUs1RyE9O8Zf+nQXljqKzw5an812cNQB2Flx4hSJJkP0ZY5xOFTHYN3ku4Waoo B3qwZwhZ/0Z1TLqM4p9UIWGPohm72ffvvW+WEIyaXX3VlDUuX3uNj10pZ3Ov3xNigf65 I7LrW/mZLK1L+Ygo5F+vb1ijvQj/6HT4g9P/kzHNEITvCoym5XWQ/tU+5YUu53KCHVvi csxA== 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=o+zvoGVHiGiVgV9+hc2BfWC8Lhc+RYzq761m+eNgLEo=; b=k0lXaPAuX+Jj8pf5HCYnF0OkZIv4VkjDSXeBepjHEYxIweq1pyNUpSLF7SvB12RvMl Gg/9hXLIX/t4vaNCdZoERy4FcFySmwOUVFf5sI3Zi4gkMCMTX1ua98W6XBN0vH1DVFOi O6L/Gsb8QM6SMFo/d955hEqMhahLfb3+f1GluDsGiiQSHJYgIcAX1MRBcGaGYMLcCXQS RLSlc45bDNM7Pfy1o4rvLq0pyx2BroJHr1L1CpnUApwltYaVtab+FJWBGasrPzQnsXm/ 1wQ4SMEZg30o/RWrsDdkSvjy8hcG+rkOjdeQWAP+PPNck/LcH5kMIrOYxWU3mlUoXwd6 rApw== 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=o+zvoGVHiGiVgV9+hc2BfWC8Lhc+RYzq761m+eNgLEo=; b=FggWvYhsM59UT1RIGPLesGw6mfGolabFXId5X+8Dqjv9cowWvq9QTaoMgjEXQ/Lg+S LOIKLs72Yt61meoo1bD34p3TSn6FafCOhbP7ytW1exaG7U8h/wJawlwUHDe5drbCGBT1 S6iau1cTia+e5F6WeXqZuhZvST3cF/OFCnIPGNaYrcrciY4nh4L+YkYN4efdfilOVTwQ VkzqMCKSZtmBkjQ4kiVs6Vn12SUYlV8gjRPqdIqojIjnJJqC6xo4teBabWxyGix7B/fA KQJORays1V2TnyWclEp6KkHCcK+i+fK3Kwo4Krc2uH/lSD8cGYmKj/5rdFfDyS9vh6Ym Q3iA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIclDQDCWzkyMN3iI922Fivoyn5TQ7Bx2DZ+C8KzsQeO7cHQW3d KO+IMzuotUW7E7jUKjpfXCQ= X-Google-Smtp-Source: AJdET5cQDDb+7qC52bBa/Rr42G7ZDOdZp0kXszHe19NiNXUwTHF+qT8BkuWqvcpFyUDncwCdstGswg== X-Received: by 2002:aca:56d0:: with SMTP id k199-v6mr71805oib.0.1541738596673; Thu, 08 Nov 2018 20:43:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:768b:: with SMTP id j11ls218328otl.5.gmail; Thu, 08 Nov 2018 20:43:16 -0800 (PST) X-Received: by 2002:a9d:3f09:: with SMTP id m9mr120515otc.5.1541738596003; Thu, 08 Nov 2018 20:43:16 -0800 (PST) Date: Thu, 8 Nov 2018 20:43:15 -0800 (PST) From: Andrew Polonsky To: Homotopy Type Theory Message-Id: In-Reply-To: References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> <5645fcc6-2520-498f-8e82-0b335d4eb3f1@googlegroups.com> Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_838_1187997192.1541738595336" X-Original-Sender: andrew.polonsky@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_838_1187997192.1541738595336 Content-Type: multipart/alternative; boundary="----=_Part_839_654961723.1541738595336" ------=_Part_839_654961723.1541738595336 Content-Type: text/plain; charset="UTF-8" The intuitive notion of a category is given by the dependently-sorted algebraic theory of categories. In the ZFC metatheory, a standard model of this theory yields the usual mathematical concept of a category. In the MLTT metatheory, a standard model of this theory yields the concept of a precategory. The subtle issue is how to treat the equality predicate, appearing in the identity and associativity axioms. In set theory, equality is a former of atomic formulae, which are a different syntactic category than sets (which interpret the types/domains of the given language). In type theory, equality is interpreted as any other type, in accordance with "the formulae-as-types notion of construction". However, more modern type theories, like HoTT or CubicalTT, have a different, "native" conception of equality, so the "natural" notion of category in these theories will accordingly be different as well. One day, there might be a metatheory which is generally accepted as providing a superior "natural" notion of a category, that avoids the awkward points of the set-theoretic one. Until then, it is best to be precise with language, always being explicit which specific concept is meant. Cheers, Andrew -- 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_839_654961723.1541738595336 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The intuitive notion of a category is given by the de= pendently-sorted algebraic theory of categories.

I= n the ZFC metatheory, a standard model of this theory yields the usual math= ematical concept of a category.

In the MLTT metath= eory, a standard model of this theory yields the concept of a precategory.<= /div>

The subtle issue is how to treat the equality pred= icate, appearing in the identity and associativity axioms.

In set theory, equality is a former of atomic formulae, which are = a different syntactic category than sets (which interpret the types/domains= of the given language).

In type theory, equality = is interpreted as any other type, in accordance with "the formulae-as-= types notion of construction".

However, more = modern type theories, like HoTT or CubicalTT, have a different, "nativ= e" conception of equality, so the "natural" notion of catego= ry in these theories will accordingly be different as well.

<= /div>
One day, there might be a metatheory which is generally accepted = as providing a superior "natural" notion of a category, that avoi= ds the awkward points of the set-theoretic one.

U= ntil then, it is best to be precise with language, always being explicit wh= ich specific concept is meant.

Cheers,
A= ndrew

--
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_839_654961723.1541738595336-- ------=_Part_838_1187997192.1541738595336--