Categories with 2-families

Categories with 2-families

[Michael Shulman]

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.
However, it seems to me that the attributes-to-families construction
can be applied to a non-discrete comprehension category as well,
producing something that one might call a "category with 2-families"
(or maybe "pseudo-families"?): a category C together with a
representable morphism Tm -> Ty of pseudofunctors C^op -> Cat.  Have
such things been defined or used anywhere before?

Re: [HoTT] Categories with 2-families

[Thomas Streicher]

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.

That's misleading I think. One rather should think categories with
attributes as full comprehension categories (like any surjective map
from a class S to Ob(C) allows one construct a category equivalent to
C whose collection of objects is S).

Thomas

Re: [HoTT] Categories with 2-families

[Peter LeFanu Lumsdaine]

[-- 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 --]

Re: [HoTT] Categories with 2-families

[Thomas Streicher]

But if you specialize the interpretation of type theory in
comprehension categories to discrete ones you wan't be able to
interpret terms (since the latter are interpreted as morphism in the
fibers, namely as sections).

So I am not sure what you mean...

Thomas

Re: [HoTT] Categories with 2-families

[Peter LeFanu Lumsdaine]

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

On Wed, Mar 7, 2018 at 9:30 PM, Thomas Streicher <
stre...@mathematik.tu-darmstadt.de> wrote:

> But if you specialize the interpretation of type theory in
> comprehension categories to discrete ones you wan't be able to
> interpret terms (since the latter are interpreted as morphism in the
> fibers, namely as sections).


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.

–p.

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

Re: [HoTT] Categories with 2-families

[Thomas Streicher]

> 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. But such guys considered as comprehension cats are full.

Maybe you just say that non-full comprehension cats are not useful for
type theory which I fully agree with! (In other contexts like fibrational
approach to geom.morph's non-full comprehensions cats are most useful but
not in full generality, one just requires the fibrations to have
comprehension which is a property not structure.)

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.

Thomas

Re: [HoTT] Categories with 2-families

[Peter LeFanu Lumsdaine]

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

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’s exactly what I mean…


> But such guys considered as comprehension cats are full.
>

…and this is exactly where I differ — CwA’s 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 —> CompCat

giving two different ways of viewing CwA’s as certain comprehension
categories, analogous to how there are two ways

D, I : Set —> Cat

of viewing sets as categories: “discrete categories” or “indiscrete
categories”.  You can say “sets are indiscrete categories”, I can say “sets
are discrete categories”, 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’s/comp cats, I’m suggesting, specifically, that the
“discrete” identification is more fruitful than has generally 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 “full split” identification without question.)

By the way, in our case, while the “discrete” viewpoint really does
identify CwA with a sub (2-)category of CompCat, the “full split” viewpoint
doesn’t, since splitness is extra structure on a fibration, and so the
“full split” functor CwA —> CompCat isn’t full, either as a functor or as a
2-functor; so the “full split” viewpoint only lets us identify 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’m saying the opposite: I’m suggesting that non-full comprehension
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’m well aware that you need strict commutation under reindexing for
term-constructors as well as for type-constructors.  But those conditions
are just as natural to state when CwA’s are viewed as discrete
comprehension categories, instead of as split full ones — if anything, they
seem to me more natural under the “discrete” viewpoint.  See point (2) in
my original email, about how logical structure on CwA’s and comp cats can
be defined more uniformly using the “discrete” identification.

–p.

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

Re: [HoTT] Categories with 2-families

[Thomas Streicher]

Dear Peter and Michael,

in full comprehension cats there is no difference between interpreting
in the fibers and interpreting in the base and that's why it doesn't
make a difference. As I said for type theoretic purposes there is not
much use for non-full comprehension cats. But I agree with Peter that
there is no point in considering non-identity morphisms in the fibers
since we interpret in the base anyway. Considering full comprehension
cats leads to unnecessary doubling of information.

Thomas

Re: [HoTT] Categories with 2-families

[Michael Shulman]

On Wed, Mar 7, 2018 at 12:30 PM, Thomas Streicher
<stre...@mathematik.tu-darmstadt.de> wrote:
> But if you specialize the interpretation of type theory in
> comprehension categories to discrete ones you wan't be able to
> interpret terms (since the latter are interpreted as morphism in the
> fibers, namely as sections).

I've never heard anyone say that terms are interpreted as morphisms in
the fibers.  For one thing, that's only possible if the fibers have
terminal objects.  It's true in the natural semantic models that a
section of the projection G.A -> G in the base category is
equivalently a map 1_G -> A in the fiber over G, and also in the
syntactic model if you have a strict unit type, but I've never heard
anyone suggest that for a general comprehension category (necessarily
with terminal objects in the fibers) the "correct" way to interpret
terms is as morphisms in the fibers rather than sections in the base.

And I'm very interested to hear you say it, because I recently came
across an application where this *does* seem to be what I want to do,
but I was hesitant because it was different from what I've heard
everywhere else.  Is there a reference that takes this point of view?

>
> So I am not sure what you mean...
>
> Thomas