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.



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


