Re: [HoTT] Is synthetic the right word?

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

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


But since this topos lies outside of the realm in which we can interpret univalent
type theory right now, we still have to rely on the infty-categorified proof to
say that we indeed know the theorem holds.

 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.

 Thierry




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