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-x33d.google.com (mail-ot1-x33d.google.com [IPv6:2607:f8b0:4864:20::33d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4cac60e5 for ; Fri, 9 Nov 2018 10:18:31 +0000 (UTC) Received: by mail-ot1-x33d.google.com with SMTP id h1sf815795oti.6 for ; Fri, 09 Nov 2018 02:18:31 -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=WgTDO0THteOhWeg0Y4A+DyKwq6ssDRphcvdpPQAg6h4=; b=TZ8rV8zOpQzCHcoGcfj2FXmrwsXsGbrh1f681QmBENMKZoFrCho61jJrgMZrxBxmd+ 1R9hd+nJCBlpg7qipG1O+rJVqgtNPHc75k89/kNmMzIjLntBWFmKgM2c4sH2uUky8bea ZwwnsQ4KW5vmaC3Xoa1h0zDByYpvS7+DTabbRwqgVP2mnCf/kWFzNQYdtcabbjnAxEoM Jv8XlNIjhxVlGdXrPIF/NI5hPm3zXccv5qmGXcs8LEMw7v03VbSpu5By8RqB7ylyMe0d Tt80AsfCNHraYp31L/fujQHbblmE7ptZJ5So8Zyz3BKTViQuK7iTl/81vz9xqRG2FKUI aBXQ== 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=WgTDO0THteOhWeg0Y4A+DyKwq6ssDRphcvdpPQAg6h4=; b=GeYAxDwVsL7qafnJaCRKYoB7WeHTwlPFRFwfEiLZ9saRMOdwDzceKbQ/IKuSb8DXt6 xrN5vWHl8xvTxmSDjDUITngO1Z56YwnMWD4lxKOsR2f7AuUw0nYVKeXQA5H3eh74clcu Wj5hD+MSZP5asChojNTxqnbfeCtZKc85yU5V5q/p3jRrH1VuKMR1BuxcHqk+IShrgrwE QzG2675H//Eel+OcRaSpO6UM8Y/PFxW89tR0Vzzlp461dsqHboOcrjutOxFMyJPbjISH JykXLCNvwG0ipM0dF3abHaM1o1OvlaGzw0alh+fVkoejs6PpW5fuICWz3j/EWtF0ETqx oDBw== 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=WgTDO0THteOhWeg0Y4A+DyKwq6ssDRphcvdpPQAg6h4=; b=UP0gomnx/QWoJ1sk38NG/kolZ51hpz6/oIW8cMKxIqnspVcwjPa6+o+Xi6grF0ShIo ZuqAIYxJck3QBEhCl/qYisrqvn4sAxkbbaBT3TexSWjitytaMatsn0sI5iBepu1Qnb6c rEqn9q0T0KuCA64c5WAduh1hwEt+2AHo02rUdn3VHKH2qRixGgvLL3+Re14kLkr3LggH pWb2JZdydqMYgmy/6+pjdgzor/aRzSsAL1PNm6Yaay6c5L6QF4wvJotYnlqOuW264IE2 aIsK1EerEMKI3WK1BgvfxbXJVquSX2lxK0UpKOxo/JPDD0FY7f7sKzQp1s3mAUom8iiR 3Iyg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gJqi+WE/VgRvivzT4KuzM+oNeH0dlb+M4axh5Yo8TFo0WDvnyos drEnpWNQGLaMIPUxl2V/CzM= X-Google-Smtp-Source: AJdET5cfi3Q/VRiIr3acxQNKBiCfH51RdUyeRRvenvL8WlbZwyxvoAAUnbPDkv5oLlPMU2d/WfIAyw== X-Received: by 2002:a9d:5ad:: with SMTP id 42mr80459otd.0.1541758710700; Fri, 09 Nov 2018 02:18:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:a8d6:: with SMTP id r205-v6ls507334oie.13.gmail; Fri, 09 Nov 2018 02:18:30 -0800 (PST) X-Received: by 2002:aca:4892:: with SMTP id v140-v6mr83007oia.1.1541758710199; Fri, 09 Nov 2018 02:18:30 -0800 (PST) Date: Fri, 9 Nov 2018 02:18:29 -0800 (PST) From: Ulrik Buchholtz 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_948_1735462796.1541758709621" 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_948_1735462796.1541758709621 Content-Type: multipart/alternative; boundary="----=_Part_949_439723200.1541758709621" ------=_Part_949_439723200.1541758709621 Content-Type: text/plain; charset="UTF-8" On Friday, November 9, 2018 at 5:43:15 AM UTC+1, Andrew Polonsky wrote: > > The intuitive notion of a category is given by the dependently-sorted > algebraic theory of categories. > Maybe for you! But not for me: I don't even know what a dependently-sorted algebraic theory is, where and how such a thing has models, nor what the particular theory you're thinking of is. But that reminds me of a MATHEMATICAL question. Consider the well-known essentially algebraic theory T whose models in Set are strict categories. What are the models of T in infinity-groupoids? (Or in an arbitrary (infinity,1)-topos?) > 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. > In cubical type theories, the two notions of equality (path types and the inductive Id-family) are equivalent, so they give equivalent notions wherever they are used. -- 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_949_439723200.1541758709621 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Friday, November 9, 2018 at 5:43:15 AM UTC+1, Andrew Po= lonsky wrote:
=
The intuitive notion of a category is given by the dependently-sorted = algebraic theory of categories.

Maybe for you! But not for me: I don't even know what a dependently-so= rted algebraic theory is, where and how such a thing has models, nor what t= he particular theory you're thinking of is.

Bu= t that reminds me of a MATHEMATICAL question. Consider the well-known essen= tially algebraic theory T whose models in Set are strict categories. What a= re the models of T in infinity-groupoids? (Or in an arbitrary (infinity,1)-= topos?)
=C2=A0
=
However, more modern type theories, like HoTT or Cubi= calTT, have a different, "native" conception of equality, so the = "natural" notion of category in these theories will accordingly b= e different as well.

In cubical= type theories, the two notions of equality (path types and the inductive I= d-family) are equivalent, so they give equivalent notions wherever they are= used.

--
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_949_439723200.1541758709621-- ------=_Part_948_1735462796.1541758709621--