From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.150.82 with SMTP id y79mr16943782iod.107.1520453726687; Wed, 07 Mar 2018 12:15:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.142.71 with SMTP id q68ls550612iod.6.gmail; Wed, 07 Mar 2018 12:15:25 -0800 (PST) X-Received: by 10.107.6.196 with SMTP id f65mr16867608ioi.69.1520453725627; Wed, 07 Mar 2018 12:15:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520453725; cv=none; d=google.com; s=arc-20160816; b=WTTDDbJybH0qQeiZbCsQIeKKpUyCQbPnpKfCaej2hnKQvVkxCBKF7Rdu0KK+Z3Tau7 lh/w7Lu9osFxWmYmnrP6ywlUgj67CHnkFux/BlV2IZuOTIOOpMzyptgUIWyVwC89vGA/ uAgTghULbEZkIFbhrdw1/ifZqw8ZKrfYiwrH2kAk93SHd+sxaaIoNsgixUuuTstXbYp6 nDlEneJE2xg6JpmRdeklfJ+GD8fhq7sOA7V+yxKRaaRD/3NX7LTd6rRwvHQVLc7i2+iu bX4S+7+WLnS0N6AZjhLje8Pb9Vd8YJB6o6rMoW1s4Knh6F12RMkVPSxMnDJ8q4GLDum1 3lYA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=J0UMAPfiBJVaiJEDIWv+4//NKFLTzMcFLDBH1sojFFc=; b=t8Bq+XoUpEbXiiG9FZmR2X+kE5AvepQt4ImsWYfmBEuPWxOnAP8VToDm3iZ95y+BIR K0nTVoUvwt+WySCgOOy/ON401S2NQAMEPwKkdhysJ7LHKPMgJCc1dH9O3TNWNdJ53s/d bHWRsvg3rJSZX2VQBA2zjHhTZT/qtgS1i756yrqiY03dcJTBeDim86fYSbsFE7y2shaW SQzMWDQ/EJI2UOY0Y9i0sgLCoC9qd5Y8X30wjljX9q9gbSuVK9YCML7iL617W3Rzy+Vo cXUoP0Bz+thGdDQYOKcvUGlyl3DZNRyEjx7RIBpexxnxph/9RAujq/a810+MRHH3900x rLew== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uzxs6j0y; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22d as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x22d.google.com (mail-vk0-x22d.google.com. [2607:f8b0:400c:c05::22d]) by gmr-mx.google.com with ESMTPS id i201si794656ite.1.2018.03.07.12.15.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Mar 2018 12:15:25 -0800 (PST) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22d as permitted sender) client-ip=2607:f8b0:400c:c05::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=uzxs6j0y; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c05::22d as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-vk0-x22d.google.com with SMTP id t126so2157542vkb.11 for ; Wed, 07 Mar 2018 12:15:25 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=J0UMAPfiBJVaiJEDIWv+4//NKFLTzMcFLDBH1sojFFc=; b=uzxs6j0yFOS13MwM6x0X1Y+/NFs9C40juSKgte0apwpJsLTHB/n0l5L8/FQ47ERfPm l+boxRECohleO23306qcjVo3agxcjsHWiB/MObkPtsXNzUTlc4nQfCmEdi/sMqiP1qfi 7AgnAjzYn+W46pZ1OAt0aXp52LaEooOYHJn/To6veu65tzDWUm5VzICEbSORb6EUV+Zs cpA6uTIwk80xKcuBeYx78XFYyKMzdbINqSrEmYLhV3n1cML9EWcP9t1SS/9vhkJxLyhE vxYEstVLNKvCx7wLEgaQQqKFZQulR19tzRK+PeUFJLqbNmlDiJJyYWfRHCJEZGR54SDG npDQ== X-Gm-Message-State: APf1xPAOzZzZxfKjG0Ba/tJvlPuXT8XD9FsMmHyN97xboepIaqfraaMd 3fTPZIUgzfrN0c8Hf9G8yRdZpyvmMD92B3PsmmI= X-Received: by 10.31.204.5 with SMTP id c5mr16680192vkg.76.1520453724940; Wed, 07 Mar 2018 12:15:24 -0800 (PST) MIME-Version: 1.0 Received: by 10.176.48.209 with HTTP; Wed, 7 Mar 2018 12:15:24 -0800 (PST) In-Reply-To: <20180307170902.GA5070@mathematik.tu-darmstadt.de> References: <20180307170902.GA5070@mathematik.tu-darmstadt.de> From: Peter LeFanu Lumsdaine Date: Wed, 7 Mar 2018 21:15:24 +0100 Message-ID: Subject: Re: [HoTT] Categories with 2-families To: Thomas Streicher Cc: Michael Shulman , "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary="001a114db1582c2e7f0566d8386e" --001a114db1582c2e7f0566d8386e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > > On Mon, Mar 05, 2018 at 01:29:56PM -0800, Michael Shulman wrote: > > By a standard construction (described for example at > > https://ncatlab.org/nlab/show/categorical+model+of+dependent+types), > > categories with families are equivalent to categories with attributes, > > i.e. to comprehension categories that are discrete fibrations. > On Wed, Mar 7, 2018 at 6:09 PM, Thomas Streicher < stre...@mathematik.tu-darmstadt.de> wrote: > > That's misleading I think. One rather should think categories with > attributes as full comprehension categories I used to agree with the usual view of CwA=E2=80=99s as full split comprehe= nsion categories, but I=E2=80=99ve come round to believing that it=E2=80=99s sign= ificantly better to view them as discrete comprehension categories (at least for most purposes). This is for several reasons: - (1) The axioms for CwA=E2=80=99s themselves, and for logical structure on= them, involve *lots* of on-the-nose equalities between types over a given context. This is perfectly natural when they=E2=80=99re seen as discrete c= omp cats (since then on-the-nose equality is the same as isomorphism in the fibre); seen as full split ones, it violates the principle of equivalence (i.e. respecting isomorphisms). - (2) The treatment of logical structure becomes more uniform between comp cats and CwA=E2=80=99s under the =E2=80=9Cdiscrete=E2=80=9D viewpoint. In = the Lumsdaine=E2=80=93Warren =E2=80=9CLocal Universes=E2=80=A6=E2=80=9D paper (https://arxiv.org/abs/141= 1.1736), where we followed the established =E2=80=9Cfull split=E2=80=9D view, we had to defin= e two separate versions of each piece of logical structure: =E2=80=9Cstrictly stable=E2=80= =9D structure as the natural notion for CwA=E2=80=99s, and =E2=80=9Cpseudo-stable=E2=80=9D s= tructure as the natural notion for comprehension cats. With the discrete viewpoint, these are a single notion: pseudo-stable structure on a discrete comp cat gives exactly strictly stable structure! - (3) 2-categorically, the picture is much nicer under the =E2=80=9Cdiscret= e=E2=80=9D view. This is a bit too much to fully describe in a quick email, but one manifestation is the fact that viewing CwA=E2=80=99s as discrete comprehens= ion categories, one gets natural inclusion 2-functors CxlCat =E2=80=94> CwA =E2=80=94> CompCat which are each 2-full-and-faithful, i.e. induce equivalences on hom-categories. Here CxlCat is the usual 1-category, viewed as a locally discrete 2-category; CwA is a fairly natural 2-category of CwA=E2=80=99s (V= oevodsky convinced me that this is much more natural than the 1-category of CwA=E2= =80=99s more usually considered); and CompCat is a 2-category in the =E2=80=9Cobvio= us=E2=80=9D way. A =E2=80=9Ctoy model=E2=80=9D of the issues involved: you can embed Set int= o Cat as either the discrete or the codiscrete categories. Viewed 1-categorically, both of these are perfectly nice full and faithful functors; but 2-categorically, while the =E2=80=9Cdiscrete=E2=80=9D embedding is 2-full-and-faithful, the = codiscrete embedding is *very* far from being so. And this can be seen as lying behind the various ways in which the =E2=80=9Cdiscrete=E2=80=9D embedding Set =E2= =80=94> Cat is more natural for almost all purposes. Going back to CwA=E2=80=99s/comp cats: the one big *advantage* I see of the= =E2=80=9Cfull split=E2=80=9D embedding is for the categorical analysis of type-constructo= rs =E2=80=94 e.g. the analysis of Pi-types and Sigma-types as adjoints =E2=80=94 since t= he constructions are on types, but their universal properties involve general context morphisms. This I agree is much cleaner under the =E2=80=9Cfull sp= lit=E2=80=9D view. On the other hand, it=E2=80=99s not lost in the =E2=80=9Cdiscrete=E2= =80=9D view =E2=80=94 e.g. it can be seen as a statement that these constructors become adjoints after applying =E2=80=9Cfullification=E2=80=9D to the discrete comp cat in questi= on. (Thankyou for bringing this issue up, by the way=E2=80=A6 I=E2=80=99ve been= looking for a good moment to air this heresy :-) ) =E2=80=93p. --001a114db1582c2e7f0566d8386e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Mon, Mar 05, 2018 at 01:29:56PM -080= 0, Michael Shulman wrote:
> By a standard construction (described for example at
> https://ncatlab.org/nlab/show= /categorical+model+of+dependent+types),
> categories with families are equivalent to categories with attributes,=
> i.e. to comprehension categories that are discrete fibrations.
=C2=A0
On Wed, Mar 7, 2018 at 6:09 PM, Thomas Str= eicher=C2=A0<stre...@mathematik.tu-darmstadt.de>=C2=A0wrote:
=C2=A0
= That's misleading I think. One rather should think categories wi= th
attributes as full comprehension categories

I used to agree with the usual view of CwA=E2=80=99s as full split compreh= ension categories, but I=E2=80=99ve come round to believing that it=E2=80= =99s significantly better to view them as discrete comprehension categories= (at least for most purposes).=C2=A0 This is for several reasons:
=

- (1)= The axioms for CwA=E2=80=99s themselves, and for logical structure on them= , involve *lots* of on-the-nose equalities between types over a given conte= xt.=C2=A0 This is perfectly natural when they=E2=80=99re seen as discrete c= omp cats (since then on-the-nose equality is the same as isomorphism in the= fibre); seen as full split ones, it violates the principle of equivalence = (i.e. respecting isomorphisms).

- (2) The treatment of logical structure beco= mes more uniform between comp cats and CwA=E2=80=99s under the =E2=80=9Cdis= crete=E2=80=9D viewpoint.=C2=A0 In the Lumsdaine=E2=80=93Warren =E2=80=9CLo= cal Universes=E2=80=A6=E2=80=9D paper (https://arxiv.org/abs/1411.1736), where we followed the establi= shed =E2=80=9Cfull split=E2=80=9D view, we had to define two separate versi= ons of each piece of logical structure: =E2=80=9Cstrictly stable=E2=80=9D s= tructure as the natural notion for CwA=E2=80=99s, and =E2=80=9Cpseudo-stabl= e=E2=80=9D structure as the natural notion for comprehension cats.=C2=A0 Wi= th the discrete viewpoint, these are a single notion: pseudo-stable structu= re on a discrete comp cat gives exactly strictly stable structure!

- (3) 2-catego= rically, the picture is much nicer under the =E2=80=9Cdiscrete=E2=80=9D vie= w.=C2=A0 This is a bit too much to fully describe in a quick email, but one= manifestation is the fact that viewing CwA=E2=80=99s as discrete comprehen= sion categories, one gets natural inclusion 2-functors

CxlCat =E2=80=94> CwA = =E2=80=94> CompCat

which are each 2-full-and-faithful, i.e. induce equivalenc= es on hom-categories.=C2=A0 Here CxlCat is the usual 1-category, viewed as = a locally discrete 2-category; CwA is a fairly natural 2-category of CwA=E2= =80=99s (Voevodsky convinced me that this is much more natural than the 1-c= ategory of CwA=E2=80=99s more usually considered); and CompCat is a 2-categ= ory in the =E2=80=9Cobvious=E2=80=9D way.
<= br>

A = =E2=80=9Ctoy model=E2=80=9D of the issues involved: you can embed Set into = Cat as either the discrete or the codiscrete categories.=C2=A0 Viewed 1-cat= egorically, both of these are perfectly nice full and faithful functors; bu= t 2-categorically, while the =E2=80=9Cdiscrete=E2=80=9D embedding is 2-full= -and-faithful, the codiscrete embedding is *very* far from being so. And th= is can be seen as lying behind the various ways in which the =E2=80=9Cdiscr= ete=E2=80=9D embedding Set =E2=80=94> Cat is more natural for almost all= purposes.


Going back to CwA=E2=80=99s/comp = cats: the one big *advantage* I see of the =E2=80=9Cfull split=E2=80=9D emb= edding is for the categorical analysis of type-constructors =E2=80=94 e.g. = the analysis of Pi-types and Sigma-types as adjoints =E2=80=94 since the co= nstructions are on types, but their universal properties involve general co= ntext morphisms.=C2=A0 This I agree is much cleaner under the =E2=80=9Cfull= split=E2=80=9D view.=C2=A0 On the other hand, it=E2=80=99s not lost in the= =E2=80=9Cdiscrete=E2=80=9D view =E2=80=94 e.g. it can be seen as a stateme= nt that these constructors become adjoints after applying =E2=80=9Cfullific= ation=E2=80=9D to the discrete comp cat in question.

(Thankyou for bringing = this issue up, by the way=E2=80=A6 I=E2=80=99ve been looking for a good mom= ent to air this heresy :-) )

=E2=80=93p.





--001a114db1582c2e7f0566d8386e--