Re: [HoTT] Categories with 2-families

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

> 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