What is the most transparent, rigorous definition of the Univalence Axiom? I've been studying homotopy type theory and trying to grasp the Univalence Axiom.  I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers that present the "flavor" of Univalence (i.e. "identity is equivalent to equivalence") but only informally.  Obviously the HoTT book has a rigorous definition but it is substantial work getting there, at least to someone new to type theory.
Can anyone give a reference to a paper that develops the minimal amount of machinery to provide a formal definition of the Univalence Axiom?
 A: I’ll give first a simplicial definition of univalence, and then a type-theoretic one, and discuss the equivalence between them as we go.
The first thing to know is that univalence is a property that can be defined for any family of types, or in models, for any fibration.  The Univalence Axiom then says that a particular family of types — a “universe” — is univalent.  I’ll come back to the universe at the end.
So: what is univalence for a fibration?  Roughly, a fibration is univalent just when the map from “paths in the base” to “equivalences between fibers” is itself an equivalence.
Precisely: given two fibrations $Y_1, Y_2$ over a common base $X$, write $\newcommand{\Hom}{\mathcal{Hom}}\Hom_X(Y_1,Y_2)$ for the fibred mapping space between them, i.e. the exponential in $\newcommand{\SSet}{\mathbf{SSet}}\SSet/X$, which represents maps between (pullbacks of) $Y_1$ and $Y_2$, and write $\newcommand{\Eqv}{\mathcal{Eqv}}\Eqv_X(Y_1,Y_2)$ for the subobject of $\Hom_X(Y_1,Y_2)$ that represents equivalences between them.  So an $n$-simplex of $\Eqv(Y_1,Y_2)$ over a simplex $x \in X_n$ corresponds to an equivalence of fibers $(Y_1)_x \to (Y_2)_x$ over $\Delta[n]$.
Now, given a single fibration $Y$ over $X$, we can consider maps between different fibers of $Y$ by first pulling it back to $X \times X$ along the two projections $\pi_1$, $\pi_2$.  So $\pi_1^*(Y)_{(x_1,x_2)} \cong Y_{x_1}$, and $\pi_2^*(Y)_{(x_1,x_2)} \cong Y_{x_2}$.  Now consider the fibred space of equivalences between these: $\Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$.  So an element of this over $(x_1,x_2)$ represents an equivalence $Y_{x_1} \to Y_{x_2}$ between fibers of $Y$.
There’s always a map $i : X \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$, living over the diagonal $\Delta_X : X \to X \times X$, where $i(x)$ represents the identity map $Y_x \to Y_x$.  Then we define: the fibration $Y \to X$ is univalent if this map $i : X \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ is a weak equivalence.
Some easily equivalent forms:


*

*(in $\SSet$, or anywhere else where cof = mono) $i$ is a trivial cofibration;

*$i$ makes $\Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ a path object for $X$;

*the induced map $P(X) \to \Eqv_{X \times X}(\pi_1^*Y,\pi_2^*Y)$ over $X \times X$ is an equivalence (for any other path object $P(X)$).


A slightly-less-trivially equivalent form is the same statement, but using an alternative construction of the object of equivalences — call it $\Eqv'_X(Y_1,Y_2)$ — which represents not just “equivalences from $Y_1$ to $Y_2$”, but “maps $f$ from $Y_1$ to $Y_2$, equipped with a homotopy left inverse $(g_l, \alpha)$ (where $\alpha$ is the homotopy $g_l \cdot f \to 1_{Y_1}$) and a homotopy right inverse $(g_r,\beta)$”.  This is equivalent to the other versions just since the evident projection $\Eqv'(Y_1,Y_2) \to \Eqv(Y_1,Y_2)$ is always a trivial fibration.
Now let’s move to type theory.  First a couple of notes about language.  It’s familiar in homotopy theory to think of a fibration as a family of spaces varying over a base space.  In type theory, this is literally the case in the language — you work with a family of types indexed by a variable varying over a base type, just like in traditional settings you work with the family of sets $\newcommand{\R}{\mathbb{R}}\newcommand{\N}{\mathbb{N}}\R^n$ indexed by $n \in \N$ — but such a family will generally behave like a fibration, not just like a discretely indexed family of discrete sets.  And in the simplicial model (and other similar models), a family of types gets interpreted as a fibration.
Also, like the HoTT book, I’ll work in prose, not in formal symbolic type theory, just like how when one does maths over a traditional foundation, one writes in prose rather than the formal symbols of first-order set theory.  (In fact the gap between prose and formal language is significantly smaller in type theory than in set-theoretic foundations, for most mathematics.)
The only basic notions we need are path types, function types, and $\Sigma$-types (types of tuples of data).
Given two types $Y_1$, $Y_2$, we can define the type $\newcommand{\tyEqv}{\mathsf{Eqv}}\tyEqv(Y_1,Y_2)$ of equivalences between them as the type of tuples $(f,g_l,\alpha,g_r,\beta)$, where $f$ is a function $Y_1 \to Y_2$, $g_l$ is a function back the other way, $\alpha$ is a function giving for each $y \in Y_1$ a path from $g_l(f(y))$ to $y$ (so $(g_l,\alpha)$ together are a homotopy left inverse for $f$), and similarly $(g_r,\beta)$ is a homotopy right inverse.  Saying a function $f : Y_1 \to Y_2$ is an equivalence means equipping it with suitable $(g_l,\alpha,g_r,\beta)$.
In general, $Y_1$ and $Y_2$ may have been dependent all along on some variable(s) — say, $Y_1(x)$ and $Y_2(x)$, where $x$ ranges over some other type $X$.  Then their interpretations in the simplicial model will be fibrations $[Y_i] \to [X]$; and $\tyEqv(Y_1(x),Y_2(x))$ is itself dependent on $x : X$, so its interpretation is also a fibration $[\tyEqv(Y_1,Y_2)] \to [X]$.  And in fact this comes out to be precisely $\Eqv'([Y_1],[Y_2])$ as defined above, since path-types are modelled by (fibred) path-objects and function types by (fibred) mapping objects.
Now for a type $Y(x)$ depending on $x:X$, and for any $x_1,x_2 : X$, there’s a canonical map $\newcommand{\tyP}{\mathsf{P}}i : \tyP_X(x_1,x_2) \to \tyEqv(Y(x_1),Y(x_2))$, defined by giving the identity equivalence $Y(x) \to Y(x)$ on reflexivity paths.  (To construct something depending on a general path, it’s enough to construct it for reflexivity paths; this is the defining property of path-types, and is analogous to extending maps defined on $X$ to maps defined on a path-object $P(X)$ along the inclusion $X \to P(X)$.)
Now, say that a family of types $Y(x)$, indexed by $x : X$, is univalent if this map $i : \tyP_X(x_1,x_2) \to \tyEqv(Y(x_1),Y(x_2))$ is an equivalence for each $x_1,x_2 : X$.
I hope the remarks so far about interpretation make it reasonably plausible, if not quite watertight, why a family of types is univalent in this sense just if its interpretation as a fibration is univalent in the simplicial sense.
Now, in type theory (as in other foundations), one often wants to consider a universe — a family of types closed under common constructions (e.g. forming function types).  Indeed, one may consider multiple such universes.  The Univalence Axiom, for a given universe, says just that this universe, considered just as a family of types, is univalent.
I’ll stop here, because this is plenty long enough already!  But a full treatment of all the above, together with the construction of univalent universes in $\SSet$, can be found in The Simplicial Model of Univalent Foundations (Kapulkin, Lumsdaine, Voevodsky).  Specifically, it’s in Section 3, using the universe introduced in in Section 2; you can probably comfortably skip Section 1, which is about the technicalities of constructing models of type theory, and also most of Section 2 after the universe is constructed.
