In Homotopy Type Theory, and more fundamentally in Martin-Löf's dependent type theory, the induction principle for identity types seems to allow the following:
Given some type $B(x,y,p)$ dependent on some $x,y:A$ and $p: x =_{A} y$, in order to construct arbitrary terms of type
$$ \Pi \ (x,y:A). (p: x =_{A} y). B(x,y,p)$$
it should suffice to give a dependent function
$$f: \Pi \ (z:A). B(z,z,r_{A}(z))$$
where $r_{A}(z) : z=_{A}z$ is the canonical reflection term.
I've come across the remark that in the homotopical interpretation, this is supposed to mean that this type theory is homotopy invariant.
How is it possible that $f$ automatically extends to $x,y:A$ off the diagonal?
How is this seeming 'existence property' constructive?
How should this phenomenon be understood logically and topologically? Where can I find a good discussion and proof of this?
Best Answer
I'll start by talking a bit about the topological interpretation of dependent type theory, I'll be brief but the details are in the HoTT book, sections 2.1,2.2 and 2.3.
Every type $A$ can be regarded as an $\infty$-groupoid, the inhabitants of $A$ are the objects of the groupoid, morphisms between $x\colon A$ and $y\colon A$ are the inhabitants of $x=_A y$, $2$-morphisms between $p,q\colon x=_A y$ are inhabitants of $p=_{x=_Ay}q$ and so on for every $n\in\Bbb N$. Now that every type has been turned into an $\infty$-groupoid we can appeal to the equivalence of categories between topological spaces up to weak homotopy equivalence and $\infty$-groupoids up to homotopy equivalence to treat every type as a topological object. If we think of inhabitants of $A$ as points of a topological space then the inhabitants of $x=_Ay$ are paths between $x$ and $y$, the inhabitants of $p=_{x=_Ay}q$ are homotopies between paths and so on. We denote with $\mathrm{refl}_x\colon x=_A x$ the constant path at $x$.
With this point of view a type family $B\colon A\to\mathcal U$ can be interpreted as a fibration with base space $A$, the fiber over $a\colon A$ is $B(a)$, the total space is $\sum_{a\colon A}B(a)$ and the space of sections is $\prod_{a\colon A}B(a)$ (it is not obvious that the homotopy lifting property required to have a fibration is satisfied, details are in section 2.3 of the HoTT book).
With this interpretation in mind we have that for $a\colon A$ the space $\sum_{y:A}y=_Aa$ corresponds to the based loop space $\Omega A$, while the type $\sum_{x,y\colon A}x=_Ay$ corresponds to the free loop space $\mathcal LA$, this makes sense since there is a fibration $\Omega A\hookrightarrow\mathcal LA\to A$. The latter type is also called the identity family over $A$, and is the type defined inductively by path induction (based path induction defines the based loop space of course). Now in the type theoretical picture we have that we only need to worry about the case $\mathrm{refl}_x\colon x=_Ax$ and in the topological picture this corresponds to the fact that every path in $\mathcal LA$ is homotopic to a constant one (just slide it to one of its endpoints!).