Simplicial sets category sSet satisfies the univalent axiom this is theorem now;with some large cardinal hypothesis. My question, Is sSet a model for Martin-lof typ theory by this theorem? any reference would be helpful.
|show 6 more comments|
You're looking for this article: http://arxiv.org/abs/1203.2553
The univalence axiom is phrased in Martin-Löf type theory. So yes, they demonstrate that the simplicial sets form a model of MLTT and moreover it models univalence.