From mboxrd@z Thu Jan 1 00:00:00 1970
X-Received: by 10.107.129.154 with SMTP id l26mr17759372ioi.48.1520460995396;
Wed, 07 Mar 2018 14:16:35 -0800 (PST)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.107.164.84 with SMTP id n81ls631848ioe.13.gmail; Wed, 07 Mar
2018 14:16:34 -0800 (PST)
X-Received: by 10.107.201.195 with SMTP id z186mr17315139iof.129.1520460994324;
Wed, 07 Mar 2018 14:16:34 -0800 (PST)
ARC-Seal: i=1; a=rsa-sha256; t=1520460994; cv=none;
d=google.com; s=arc-20160816;
b=dySH00ZyGnfWEqV2vVIarMTF4Cjnr/p/TMWGf/XZrWjt6GfcWGQiExrUu8zPA757as
Ba70JZ0TjYAUIUD1cUG6ZVBmEfwPhkuoMlNmX3F8SBnaJyGTfBcn3FOJX/fOnhdBpef5
b74xS1GrCom6iqrTlSsjOOorbyBA9UGS/U6es8MTLRgvzRuiEYbqbKHr9FivhQrYzp3x
7FiA1R7aeIPA3easi5swpMgXkykqRdo3vFVEtqBNO6b78bt9ZqkoCQF96I3qTBzjKUtU
VwL13BhYVtIn28K5vDCimLS4dgdMX7Juym8SkwsCIDZYYnKQY8VPSMbJhF/2XUcFwwmQ
vwwg==
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=FfQUjmAS9BJL+D03EQRqD/8UAz4smMihHqW4edfXUH0=;
b=C3sgPOBFCUSNrOUdgvgg2HZuCiO0cAcG1GKLa8cD7InzUneuKFJCQCb/40xZ+49ShL
+M3w8OP2nBDz1VQKpeQ3WyS++2ak/8KOOnWacunadKwMxjY1ogm/nR2aFo5Ad+WpoCDy
/5n/4YCbopRUak5ShLrn9uZqauK7WV7x93V00kvcfU5lwY4M1bycOyDChLXoP4tbKx9n
T8WY/IRlSO+hJS3e9waZXA2ViorA6DPm+gjjIEH1Kobs3uiYGHKic3yD1nFYyoTnuyEi
TOrEf1gAN2UcAd/708PJuYt9CBy7EobydySfbBqQ4YzGDOebK+s3qadwm0vaBMT+Ec3A
oS4w==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
dkim=pass head...@gmail.com header.s=20161025 header.b=OmOe3t5l;
spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22a 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-ua0-x22a.google.com (mail-ua0-x22a.google.com. [2607:f8b0:400c:c08::22a])
by gmr-mx.google.com with ESMTPS id n15si930887ith.0.2018.03.07.14.16.34
for
(version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
Wed, 07 Mar 2018 14:16:34 -0800 (PST)
Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22a as permitted sender) client-ip=2607:f8b0:400c:c08::22a;
Authentication-Results: gmr-mx.google.com;
dkim=pass head...@gmail.com header.s=20161025 header.b=OmOe3t5l;
spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::22a 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-ua0-x22a.google.com with SMTP id c14so2566734uak.7
for ; Wed, 07 Mar 2018 14:16:34 -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=FfQUjmAS9BJL+D03EQRqD/8UAz4smMihHqW4edfXUH0=;
b=OmOe3t5lPwFBjtvNtNclAf/RoKyTLAOmEeAYXHZ6gKo4ar5UdgtSFsb7uF+KrhlmTo
d+L1JFb8fIp0uglX/ydZLfqlfgl7fh4hWVUbtqD4vJAFwuayK7GqKAIT3x74nJJyryoE
3NJBjfeKsXL+aix3M1gBOnMBtxXM6yTLZUGitrez21Dr026lJwZ8wrGYupOu2z9p3sQc
OYfMv2JwddaEIEdZWKBBzpEZNm3IT/SEZSww4UOGpYYJvWFWFZ5Z66Bs08g44tfLjajP
4Nv7TsZ5sXaImGLXWoNEueADG4mms68KnWGwdAbpaqrv6vbhcPJpRcC+gV3rRQNINKMN
Wp4A==
X-Gm-Message-State: APf1xPCE7bG677hnSVsgMBKOq7UcyeNdxEX/U7AW8ke1e9+ymaFAnnMi
Kt/OyoGYTNkEyWQb6x20O//9dTxHF2kzrOxOqLs=
X-Received: by 10.159.49.27 with SMTP id m27mr18062306uab.169.1520460992813;
Wed, 07 Mar 2018 14:16:32 -0800 (PST)
MIME-Version: 1.0
Received: by 10.176.48.209 with HTTP; Wed, 7 Mar 2018 14:16:32 -0800 (PST)
In-Reply-To: <20180307210109.GA12590@mathematik.tu-darmstadt.de>
References:
<20180307170902.GA5070@mathematik.tu-darmstadt.de>
<20180307203003.GA11083@mathematik.tu-darmstadt.de>
<20180307210109.GA12590@mathematik.tu-darmstadt.de>
From: Peter LeFanu Lumsdaine
Date: Wed, 7 Mar 2018 23:16:32 +0100
Message-ID:
Subject: Re: [HoTT] Categories with 2-families
To: Thomas Streicher
Cc: Michael Shulman ,
"HomotopyT...@googlegroups.com"
Content-Type: multipart/alternative; boundary="f403045ddf745f20970566d9e9e7"
--f403045ddf745f20970566d9e9e7
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
On Wed, Mar 7, 2018 at 10:01 PM, Thomas Streicher <
stre...@mathematik.tu-darmstadt.de> wrote:
> > To clarify, by ???discrete comprehension categories??? I mean the ones
> Mike was
> > talking about, i.e. where the fibration of types is a discrete
> fibration; I
> > don???t mean that the base category is discrete. So there???s no
> problem here
> > ??? terms are still interpreted as sections of dependent projections,
> just as
> > usual.
>
> Ok, that's like interpretation in categories with attributes, where
> terms are interpreted in the base and only types in the fibers of the
> presheaf of types.
Yes, that=E2=80=99s exactly what I mean=E2=80=A6
> But such guys considered as comprehension cats are full.
>
=E2=80=A6and this is exactly where I differ =E2=80=94 CwA=E2=80=99s can be =
identified with full
split comp cats, but they can also (differently) be identified with
discrete comprehension categories. That is, there are TWO very natural
(2-)functors
D, F : CwA =E2=80=94> CompCat
giving two different ways of viewing CwA=E2=80=99s as certain comprehension
categories, analogous to how there are two ways
D, I : Set =E2=80=94> Cat
of viewing sets as categories: =E2=80=9Cdiscrete categories=E2=80=9D or =E2=
=80=9Cindiscrete
categories=E2=80=9D. You can say =E2=80=9Csets are indiscrete categories=
=E2=80=9D, I can say =E2=80=9Csets
are discrete categories=E2=80=9D, and neither of us is absolutely right or =
wrong;
one can identify Set with either of those two different subcategories of
Cat, and each of these identifications is useful for some purposes.
Back with CwA=E2=80=99s/comp cats, I=E2=80=99m suggesting, specifically, th=
at the
=E2=80=9Cdiscrete=E2=80=9D identification is more fruitful than has general=
ly been
appreciated. (Almost all literature I know on comprehension categories,
including my own paper with Michael Warren on them that I referenced
before, uses the =E2=80=9Cfull split=E2=80=9D identification without questi=
on.)
By the way, in our case, while the =E2=80=9Cdiscrete=E2=80=9D viewpoint rea=
lly does
identify CwA with a sub (2-)category of CompCat, the =E2=80=9Cfull split=E2=
=80=9D viewpoint
doesn=E2=80=99t, since splitness is extra structure on a fibration, and so =
the
=E2=80=9Cfull split=E2=80=9D functor CwA =E2=80=94> CompCat isn=E2=80=99t f=
ull, either as a functor or as a
2-functor; so the =E2=80=9Cfull split=E2=80=9D viewpoint only lets us ident=
ify CwA with a
sub (2-)category of CompCat_spl, not of CompCat.
Maybe you just say that non-full comprehension cats are not useful for
> type theory which I fully agree with!
>
No, I=E2=80=99m saying the opposite: I=E2=80=99m suggesting that non-full c=
omprehension
cats, and the discrete in particular, are *more* useful for type theory
than we have generally realised before!
But it's not enough to require the splitting for types. One also has
> to require it for the associate FULL comprehension cat. E.g. it's not
> sufficient to have it for Pi, you must also have it for eval.
I=E2=80=99m well aware that you need strict commutation under reindexing fo=
r
term-constructors as well as for type-constructors. But those conditions
are just as natural to state when CwA=E2=80=99s are viewed as discrete
comprehension categories, instead of as split full ones =E2=80=94 if anythi=
ng, they
seem to me more natural under the =E2=80=9Cdiscrete=E2=80=9D viewpoint. Se=
e point (2) in
my original email, about how logical structure on CwA=E2=80=99s and comp ca=
ts can
be defined more uniformly using the =E2=80=9Cdiscrete=E2=80=9D identificati=
on.
=E2=80=93p.
--f403045ddf745f20970566d9e9e7
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
--f403045ddf745f20970566d9e9e7--