In Martin-Löf type theory with identity eliminator


$$
J :
\prod\_{B:\prod\_{x,y:A}(x=y)\to\mathcal{U}}\left(
\prod\_{x:A}B(x,x,\mathrm{refl}\_x)\to 
\prod\_{x,y:A}\prod\_{p:x=y}B(x,y,p)
\right)
$$


satisfying $J(B,b,x,x,\mathrm{refl}\_x)=b(x)$ we can have terms $p:x=x$ that are not equal to $\mathrm{refl}\_x$. 


We can then interpret the $x:A$ as points of a space, and the terms of $x=y$ as the paths joining $x$ and $y$. The loops $p:x=x$ that are not $\mathrm{refl}\_x$ are interpreted as non-contractible loops. Terms of type $p=\_{x=y}q$ are homotopies between paths, etc.


Now, I have seen that the univalence axiom is of great importance in homotopy type theory, but I don't see how it enters in this discussion. The question is: does univalence have consequences in the homotopy interpretation of type theory?


If the answer is yes, what role does it play?



The role of univalence in the homotopy interpretation of type theory
Whenever you’re looking at a logical system, there’s a tension between two main ways of studying it:


* axioms/theorems in the system show what the world it describes *must* look like;
* models show what the world it describes *can* look like.


The interpretation of types as spaces shows that the types of plain Martin-Löf type theory *can* look like homotopically non-trivial spaces (unlike e.g. the sets of ZF(C), which are always homotopically discrete).


However, in plain Martin-Löf type theory, you can’t prove that there *must* exist homotopically non-trivial types. It’s consistent that every type “is a set”, in the sense of being homotopically discrete. This follows from the fact that you can also model types as plain old sets, in ZF(C) or any similar theory.


**Univalence implies that there *must* exist homotopically non-trivial types.** Specifically, once you add both univalence and higher inductive types, then (as shown in the HoTT book, and various papers on synthetic homotopy theory) you can reproduce many standard constructions of spaces from classical homotopy theory, and show that they behave how you’d expect them to in many ways: e.g. that the fundamental group of the circle is $\mathbb{Z}$, just to name the simplest non-trivial such fact.


So from the point of view of the homotopy interpretation of type theory, the rôle of univalence is ensuring that enough homotopically non-trivial types exist for the world to look like a reasonable homotopy-theoretic world. One approach to making this precise is to say that univalence should force the universe (or a hierarchy of universes, or something) to be an *object classifier* (or classiying family, or something) in the sense of Lurie’s ∞-topos theory — though this idea hasn’t been made precise yet.


This isn’t the only rôle of univalence: it’s not Voevodsky’s original motivation, for example. That was roughly, as I understand it, to allow more powerful and natural reasoning about how constructions respect equivalence, because pragmatically one often needs to use such reasoning when formalising mathematics in type theory. But it’s the essential rôle that univalence plays from the point of view of the homotopy-theoretic interpretation.


