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.