Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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|improve this question
2  
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

1 Answer 1

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.

share|improve this answer

Your Answer

 
discard

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.