Re: [HoTT] Categories with 2-families

[Michael Shulman <shu...@sandiego.edu>]

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