Hi Thierry,


>  A small remark about this: at least we can interpret type theory with the
> univalence
> axiom in the (iterated) presheaf category
>
>  [Fin_*, [C^op, Set]]
>
> where C is the category of cubes we have considered for cubical type theory
> (since we know how to interpret universes in presheaf categories and all
> the operations
> relativize to presheafs; on the other hand, it is not clear yet how to
> relativize it for -sheaf- models
> since it is less clear how universes should be interpreted).
> We also should have a purely syntactical version, where judgements are
> indexed not only over a finite set
> but over a pair of a finite set and a pointed finite set.
>
>
Very interesting remark.

I'm not quite sure this quite corresponds to what I had in mind, since I
was thinking of the
infty-category of presheaves on the infty-category of finite pointed
spaces.  (That is,
by Fin_* I mean finite *spaces*, not finite sets... sorry if my notation
was bad)  With this in mind, I guess
in the remark this would correspond to something like considering the
"enriched"
presheaves with some chosen model structure.  But I'm getting a bit out of
my depth here
so maybe someone can chime in to help me out ...

So it looks to me like you are saying something like that the cubical model
should tell
us how to interpret type theory in an infinity-topos of presheaves on an
arbitrary 1-category?
Is this right, or am I misunderstanding? Or was Fin_* special for some
reason (though,
again, Fin_* for me was finite spaces, not finite sets ...)?  Can I replace
Fin_* with D for any category D?

Fin_* certainly falls outside of the EI-category restriction, and I was not
aware that
we knew how to lift that.  Does cubical type theory give a way or have I
completely missed the point?  :p

Cheers,

Eric