# sSet is a model for Martin-lof type theory

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.

-
what is the univalent axiom? In what sense do you mean that sSet is a model for constructive mathematics? as a topos? – Ittay Weiss Jan 10 '13 at 6:57
I mean, Voevodsky's univalent axiom and Martin-Lof's constructive mathematics – user56768 Jan 10 '13 at 7:13
Sorry, as a topo – user56768 Jan 10 '13 at 7:21
Homotopy type theory is an extension of Martin–Löf type theory, so I suppose the answer is yes in principle... – Zhen Lin Jan 10 '13 at 7:42
@ZhenLin:do you mean that; Martin-lof type theory does not need strong hypothesis – user56768 Jan 10 '13 at 8:06