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.

mustunderstand type theory first – at minimum the notion of identity types. I think it would be enough to read Chapter 1 of the HoTT book, then skip to §2.10. $\endgroup$ – Zhen Lin Jun 30 '15 at 19:03