Re: [HoTT] Is synthetic the right word?

[Thierry Coquand <Thierry...@cse.gu.se>]

[-- Attachment #1: Type: text/plain, Size: 2227 bytes --]


 Sorry for the misunderstanding!  Indeed, what I wanted to state was only
something corresponding to

 -how to interpret type theory in an infinity-topos of presheaves on an arbitrary 1-category-

 and I misread what you wrote reading “finite set” instead of “finite space”...
    Thierry

On 16 Jun 2016, at 19:51, Eric Finster <ericf...@gmail.com<mailto:ericf...@gmail.com>> wrote:

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


[-- Attachment #2: Type: text/html, Size: 5127 bytes --]