where

$isequiv(f) \equiv \left(\Sigma_{g:B\to A}(f\circ g\sim id_B)\right) \times \left(\Sigma_{g:B\to A}(h\circ f\sim id_A)\right)$

where

$(k\sim l)\equiv \Pi_{x:C} \left(k(x)=_{P(x)}l(x)\right)$

where

$P:C\to U$ and $k,l: \Pi_{x:C}P(x)$.

We see how equivalence of types $(A\simeq B)$ eventually comes down to equality of terms.

(The univalence axiom then says that to find those term-equalities, one can construct an equivalence on of these terms.)

This is in analogy to how equivalences of categories (defined via natural isomorphisms) comes down to isomorphisms of objects.

Identity type