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.