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.
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.
Here's how it works:
- Anybody can ask a question
- Anybody can answer
- The best answers are voted up and rise to the top
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.