univalent axiom as a property of a model category?  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.
 A: 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.
A: 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 )
A: 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. 
