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.