Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
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

You're looking for this article:

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.