5
$\begingroup$

I am interested to understand the univalence axiom of Voevodsky; however, I know very little type theory. Thanks to response below, I now understand what is being univalent means for a morphism. A couple more questions, though:

Do I understand correctly that tthe Univalence Axiom makes sense for an arbitrary locally cartesian closed model category ? And what is 'the universe of small fibrations'? If I understand correctly, it means that for each small fibration g:Y→X there are morphisms h:X→U and h˜:Y→U˜ such that the corresponding square is a pull-back square. What does exactly 'small' mean here?

Is there a reformulation of the univalence axiom stated fully in terms of a model category, perhaps with an distinguished fibration ? What is the best reference giving full detail?

I was not able to find anything in the literature. The NSF proposal of Voevodsky seem to come quite close to giving such a formulation, but it does not have full details.

Improve this question
$\endgroup$

3 Answers 3

Reset to default
3
$\begingroup$

The Univalence Axiom states that the universe of small fibrations $\pi:\tilde{U}\to U$ is a univalent fibration. Let a fibration $p:E\to B$ be given. If the underlying model category is locally cartesian closed, then you can form the map $Path_{w}(B)\to B\times B$ over $B\times B$ which has as fiber over $(b,b')$ the object of weak equivalences $E_{b}\to E_{b'}$ between fibers. There is a map $m:B\to Path_{w}(B)$ which sends $b$ to the identity map $E_{b}\to E_{b}$. $p$ is univalent if and only if the map $m$ is a weak equivalence.

Improve this answer
$\endgroup$
8
  • $\begingroup$ Thanks! I understand now what is being 'univalent' means fro a fibration. A couple of questions: do I understand correctly that this definiton makes sense for an arbitrary locally cartesian closed model category ? And what is 'the universe of small fibrations'? If I understand correctly, it means that for each small fibration $g:Y\rightarrow X$ there are morphisms $h:X\rightarrow U$ and $\tilde h:Y\rightarrow \tilde U$ such that the corresponding square is a pull-back square. What does exactly 'small' mean here? $\endgroup$
    – o a
    Commented Aug 18, 2011 at 12:25
  • $\begingroup$ The universe of small fibrations is as you say the classifying small fibration. The notion of "small" here should be understood in terms of algebraic set theory and for presheaf model categories a map can be defined to be small provided that all of its fibers are small sets (in the sense of a Grothendieck universe or large cardinal, which we are assuming if we want to model universe). So roughly, what one needs is a locally cartesian closed model category with a suitable notion of small map. $\endgroup$
    – Michael A Warren
    Commented Aug 18, 2011 at 15:56
  • $\begingroup$ There are a few other subtle issues ($m$ should be a cofibration also, one must see how internal/type theoretic and external/homotopical weak equivalences are related) which one must verify. Regarding your question about the literature, there is, as far as I know, no other source of literature on these matters other than Voevodsky's papers and notes and Mike Shulman's blog posts on the n-cafe. (That said, Peter LeFanu Lumsdaine and I are working on a paper at the moment which details how many of these things work in the case of model category structures on presheaf and sheaf toposes.) $\endgroup$
    – Michael A Warren
    Commented Aug 18, 2011 at 15:58
  • $\begingroup$ another question: how does one define Path_w(B) in an arbitrary cartesian closed model category? $\endgroup$
    – o a
    Commented Oct 10, 2011 at 17:11
  • $\begingroup$ Could it be that the locally cartesian model categories satisfying the univalent axiom are the really just the same thing as the (infty,1)-topoi, in the sense of Toen-Vezzosi/Lurie? $\endgroup$
    – Charles Rezk
    Commented Oct 10, 2011 at 23:00
2
$\begingroup$

Maybe this is helpful

http://www.cs.man.ac.uk/~petera/Recent-Slides/Edinburgh-2011-slides_pap.pdf

Also, snipping from email to socalfp google group, there's a 3 video Institute for Advansted Studies series connected to this at

http://video.ias.edu/univalent

1) Steve Awodey, Contructive Type Theory and Homotopy (still working through)

2) Andrew Appel, Introduction to Coq Proof Assistant (watched, covers much of the material we've already done, from early chapters of Pierce's SF, also an interesting QA at the end where Appel describes his own use of coq in certifying properties of compilers and virtual machines iirc )

3) Vladimir Voevodsky, Univalent Foundations of Mathetmatics (watched, brief explanation of what "homotopy levels" mean, then many screens of Coq explainng how this relates to homotopy theory. My eyes glazed over. maybe this will make more sense after watching Awodey's video (1) )

For those with some category theory, it may be helpful to note that groupoids are categories where all morphisms are invertible, since groupoids seem to play a key role in homotopy theory, and groupoid-ish jaron is favored, rather than more familiar (to me) category jargon. ( hen.wikipedia.org/wiki/Groupoid )

Improve this answer
$\endgroup$
2
$\begingroup$

This note in arxiv:1111.3489 gives an formal interpretation of the univalence axiom in an arbitrary (locally cartesian closed) model category: basically, interpret word-by-word a passage of Voevodsky describing the univalence for sSets. The authors are non-specialist, though, so various blunders possible.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .