Associativity of cartesian product in Univalent Foundations In classical set theory, pairs $(x,y)$ are encoded usually in such a way that (for sets $A,B,C$)
$(A\times B)\times C \neq A\times (B\times C)$. 
From my (small) knowledge of Univalent foundations, objects do not carry "extra information" (such that $1\in 2$...), my question is thus : 
Do we have equality $(A\times B)\times C = A\times (B\times C)$ in the setting of Univalent foundations?
 A: Yes. If $X$ and $Y$ are types, the univalence axiom provides a way to construct a witness of the equality $X = Y$ given any equivalence $\varphi\colon X\simeq Y$. Isomorphisms of $X$ with $Y$ give in particular equivalences of $X$ with $Y$. It hence suffices to construct $f\colon (A \times B) \times C \to A \times (B \times C)$ and a function $g$ in the other direction such that $f$ and $g$ are pointwise inverses of each other.
But this is possible due to the definition of (or the axioms for) product types of the form $X \times Y$. For this product type we know:


*

*For terms $x \in X$ and $y\in Y$, we may construct a term $(x,y)\in X\times Y$

*We have functions $\pi_1 \colon X \times Y \to X$ and $\pi_2 \colon X \times Y \to Y$ such that for all $p \in X\times Y$ we have $p = (\pi_1(x),\pi_2(y)).$
Hence I'm allowed to define $f\colon (A \times B) \times C \to A \times (B \times C)$ by $(p,c) \mapsto (\pi_1(p),(\pi_2(p),c))$. This is the usual isomorphism, for which one constructs the usual pointwise inverse $g$.
