1
$\begingroup$

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.

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

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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