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