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.