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-x239.google.com (mail-oi1-x239.google.com [IPv6:2607:f8b0:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8ea21901 for ; Fri, 9 Nov 2018 10:58:01 +0000 (UTC) Received: by mail-oi1-x239.google.com with SMTP id g138-v6sf744346oib.14 for ; Fri, 09 Nov 2018 02:58:01 -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=0iMZaBV8LsCfhz5i/aXs7CzTn9l80JO2G35lvAaf8to=; b=q1Fj+cmT4zmJlL8WawFcDBg08mHSekU2wa1o4XN4Eo1M0kWmAFpO4YLj01/LvbQ6Q3 3rGm4752MMJyD0f7wP62cEI8jguNNJ1urvSEIb45afNCmfGJ+Iypnijtl2XBOH9pZ0em iBulblOdNGHiVxN1YLLvPYLJEBo9jakYk/+VcbzhZG6dFl6V0qZSmgcBMVB0Bv/eerZf zieN2aYBSin9OAwDcs6DlZ2EgIQjPQx8orV8QKmYXzs575R5A1l+fyv5FWHy66Bs+ga/ HrK1RNK4Qv6aix7zEjrifOfVIerHY64mg/RcDQK97ovJnvl5w88VhDZPoYIFJNS6xP6+ 6vRA== 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=0iMZaBV8LsCfhz5i/aXs7CzTn9l80JO2G35lvAaf8to=; b=pCkQz5y41NHvLTs9M8JV60RGQrm0D4l9dH65fCHuml4yC4hLf7wbridyTxfcKHXNQN tBKnqRF7O5SsgC89dCWHKTdM3mAq5YZsnsNlB65CJ0U9eVy5ZVZ70TJS/n8Vr/H7dwsJ BniK0jEz9ID86l76NSCJ+JRVwKWyBpVm9mINH0caXuewwiYP1UctEwkWnC80zoQOcT67 KyEuOWte6dRQStt24HaHQGwXCUE6ZdIKP4fmwDCrzWOMWBYNCbK0MNo+OB00HzTSwq6j UQtC4V9xqgkTSOh8GvXiOB0nLqTyxcFbXmIVpasriDN+JqNwySbkWxIRdmu+ymkg0uaH AwHg== 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=0iMZaBV8LsCfhz5i/aXs7CzTn9l80JO2G35lvAaf8to=; b=SvPCUoFJqkvCOS0zZiN/tLPtEynK97Pnd3uy3dACS0cR/aPFoeps8PDiTfwx8osCAt kZ95LHnOyfsmIQEIq+wcun6oo/pXCD3iNzyCod29t4tll/+p6TUuJfY9JHWqBCClpc51 JyCYBSfU7MU5x9k/677v1wVb26bFAFTmdlNtSQy11zyDTjnPD5K74A6MuQvY1Y8hNbPF dWFuy5ISyLCKuBEAgXnhACPd8lbn5lDJ3bB4tSTs128Uu7t1BRH5ikC1kMJDEihz+UFu T/8iSFM2unVcQHGTTl/Y0rRyu9+0JmqIdHoRDQ/25CMMn4gIPlfi7PixKPL3rU/jVZK0 ijbA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIACyeDj4azNrXF0Fbqinq9ef6Q/Wh7QHisq7k1+kbrMAbUERZ7 M38sBwHR4DZ4YBcwFLxJYjI= X-Google-Smtp-Source: AJdET5c/bAB45WYLgwoKVmaQenqRwIxswSekB+pCAnbdvZyA08O9bFZI90c7EEvcF6uGK5S7rCSDew== X-Received: by 2002:a9d:5ad:: with SMTP id 42mr82630otd.0.1541761080897; Fri, 09 Nov 2018 02:58:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5085:: with SMTP id e127-v6ls509981oib.11.gmail; Fri, 09 Nov 2018 02:58:00 -0800 (PST) X-Received: by 2002:aca:a984:: with SMTP id s126-v6mr27616oie.6.1541761080400; Fri, 09 Nov 2018 02:58:00 -0800 (PST) Date: Fri, 9 Nov 2018 02:57:59 -0800 (PST) From: Paolo Capriotti To: Homotopy Type Theory Message-Id: <7d2c4275-af39-44c4-81ae-9be921b9318e@googlegroups.com> 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_762_1527211934.1541761079746" X-Original-Sender: p.capriotti@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_762_1527211934.1541761079746 Content-Type: multipart/alternative; boundary="----=_Part_763_756656889.1541761079746" ------=_Part_763_756656889.1541761079746 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Fri, 9 Nov 2018, at 10:18 AM, Ulrik Buchholtz wrote: > 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= =20 > > algebraic theory of categories. > > > > Maybe for you! But not for me: I don't even know what a dependently-sorte= d > algebraic theory is, where and how such a thing has models, nor what the > particular theory you're thinking of is. Let's say we define a *dependently-sorted algebraic theory* to just be a=20 CwF. A model for it is a CwF-morphism into Set (or more generally into a=20 CwF). The theory of categories would then be the opposite of Cat_{fp} (I=20 mean finitely presentable, *not* locally finitely presentable), or=20 alternatively you can define it inductively as the syntax of a type theory= =20 (but then you have to prove an initiality theorem!). I'm not sure how this kind of presentation translates to =E2=88=9E-categori= es=20 though. > But that reminds me of a MATHEMATICAL question. Consider the well-known= =20 > essentially algebraic theory T whose models in Set are strict categories.= =20 > What are the models of T in infinity-groupoids? (Or in an arbitrary=20 > (infinity,1)-topos?) Nice question! I guess by model here you mean a left exact =E2=88=9E-functor T =E2=86=92 S= pace, where T is=20 regarded as an ordinary category with finite limits. I think such models=20 are equivalent to Segal spaces, but without completeness. Or at least, I=20 don't see where completeness would come from. I find it quite an illuminating way to look at Segal spaces, by the way.=20 You get the space of n-simplices by mapping the iterated pullback of the=20 object of arrows in T (i.e. the object that stands for sequences of=20 composable arrows). The Segal condition is the preservation of that=20 pullback. It's essentially the same idea as in the definition of =CE=93-Spa= ces. Best, Paolo --=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_763_756656889.1541761079746 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Fri, 9 Nov 2018, at 10:18 AM, Ulrik Buchholtz= wrote:
> On Friday, November 9, 2018 at 5:43:15 AM UTC+1, And= rew Polonsky wrote:
> >
> > The intuitive n= otion of a category is given by the dependently-sorted=C2=A0
>= > algebraic theory of categories.
> >
>
> Maybe for you! But not for me: I don't even know what a de= pendently-sorted
> algebraic theory is, where and how such a t= hing has models, nor what the
> particular theory you're t= hinking of is.

Let's say we define a *dependen= tly-sorted algebraic theory* to just be a CwF. A model for it is a CwF-morp= hism into Set (or more generally into a CwF). The theory of categories woul= d then be the opposite of Cat_{fp} (I mean finitely presentable, *not* loca= lly finitely presentable), or alternatively you can define it inductively a= s the syntax of a type theory (but then you have to prove an initiality the= orem!).

I'm not sure how this kind of presenta= tion translates to =E2=88=9E-categories though.

&g= t; But that reminds me of a MATHEMATICAL question. Consider the well-known= =C2=A0
> essentially algebraic theory T whose models in Set ar= e strict categories.=C2=A0
> What are the models of T in infin= ity-groupoids? (Or in an arbitrary=C2=A0
> (infinity,1)-topos?= )

Nice question!

I guess = by model here you mean a left exact =E2=88=9E-functor T =E2=86=92 Space, wh= ere T is regarded as an ordinary category with finite limits. I think such = models are equivalent to Segal spaces, but without completeness. Or at leas= t, I don't see where completeness would come from.

=
I find it quite an illuminating way to look at Segal spaces, by t= he way. You get the space of n-simplices by mapping the iterated pullback o= f the object of arrows in T (i.e. the object that stands for sequences of c= omposable arrows). The Segal condition is the preservation of that pullback= . It's essentially the same idea as in the definition of =CE=93-Spaces.=

Best,
Paolo

<= /div>

--
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_763_756656889.1541761079746-- ------=_Part_762_1527211934.1541761079746--