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
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 t= he 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.=C2=A0 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 exac= tly what I mean=E2=80=A6
=C2=A0
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 als= o (differently) be identified with discrete comprehension categories.=C2=A0= That is, there are TWO very natural (2-)functors

= D, F : CwA =E2=80=94> CompCat

giving two differ= ent ways of viewing CwA=E2=80=99s as certain comprehension categories, anal= ogous 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.= =C2=A0 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 ab= solutely right or wrong; one can identify Set with either of those two diff= erent 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, that the =E2=80=9Cdiscrete=E2=80=9D = identification is more fruitful than has generally been appreciated. =C2=A0= (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 question.)

<= /div>
By the way, in our case, while the =E2=80=9Cdiscrete=E2=80=9D vie= wpoint really 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 ext= ra structure on a fibration, and so the =E2=80=9Cfull split=E2=80=9D functo= r CwA =E2=80=94> CompCat isn=E2=80=99t full, either as a functor or as a= 2-functor; so the =E2=80=9Cfull split=E2=80=9D viewpoint only lets us iden= tify CwA with a sub (2-)category of CompCat_spl, not of CompCat.
=
Maybe you just say that non-full c= omprehension cats are not useful for
type theory which I fully agree with!

N= o, I=E2=80=99m saying the opposite: I=E2=80=99m suggesting that non-full co= mprehension cats, and the discrete in particular, are *more* useful for typ= e 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.
<= div>
I=E2=80=99m well aware that you need strict commutation = under reindexing for term-constructors as well as for type-constructors.=C2= =A0 But those conditions are just as natural to state when CwA=E2=80=99s ar= e viewed as discrete comprehension categories, instead of as split full one= s =E2=80=94 if anything, they seem to me more natural under the =E2=80=9Cdi= screte=E2=80=9D viewpoint.=C2=A0 See point (2) in my original email, about = how logical structure on CwA=E2=80=99s and comp cats can be defined more un= iformly using the =E2=80=9Cdiscrete=E2=80=9D identification.

=
=E2=80=93p.


--f403045ddf745f20970566d9e9e7--