Re: [HoTT] Categories with 2-families

[Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3826 bytes --]

>
> 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’s as full split comprehension
categories, but I’ve come round to believing that it’s significantly better
to view them as discrete comprehension categories (at least for most
purposes).  This is for several reasons:

- (1) The axioms for CwA’s 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’re seen as discrete comp 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’s under the “discrete” viewpoint.  In the Lumsdaine–Warren
“Local Universes…” paper (https://arxiv.org/abs/1411.1736), where we
followed the established “full split” view, we had to define two separate
versions of each piece of logical structure: “strictly stable” structure as
the natural notion for CwA’s, and “pseudo-stable” structure 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 “discrete”
view.  This is a bit too much to fully describe in a quick email, but one
manifestation is the fact that viewing CwA’s as discrete comprehension
categories, one gets natural inclusion 2-functors

CxlCat —> CwA —> 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’s (Voevodsky
convinced me that this is much more natural than the 1-category of CwA’s
more usually considered); and CompCat is a 2-category in the “obvious” way.


A “toy model” of the issues involved: you can embed Set into 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 “discrete” 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 “discrete” embedding Set —> Cat is more
natural for almost all purposes.


Going back to CwA’s/comp cats: the one big *advantage* I see of the “full
split” embedding is for the categorical analysis of type-constructors —
e.g. the analysis of Pi-types and Sigma-types as adjoints — since the
constructions are on types, but their universal properties involve general
context morphisms.  This I agree is much cleaner under the “full split”
view.  On the other hand, it’s not lost in the “discrete” view — e.g. it
can be seen as a statement that these constructors become adjoints after
applying “fullification” to the discrete comp cat in question.

(Thankyou for bringing this issue up, by the way… I’ve been looking for a
good moment to air this heresy :-) )

–p.

[-- Attachment #2: Type: text/html, Size: 5448 bytes --]