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
--001a114db1582c2e7f0566d8386e--