# Induction on identity types in HoTT and dependent type theory

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?

• I'll leave it to someone else to explain the motivation and connections with homotopy. But in answer to your questions "How is it possible that $f$ automatically extends to $x,y:A$ off the diagonal?" and "Where can I find a good ... proof of this?" This is just one of the rules of HoTT, the elimination rule for equality types. It's possible because that's how the system works, and you can give a one-line proof: apply the elimination rule. – Alex Kruckman Jun 29 '19 at 15:24
• Also, if you have $x,y:A$ and $p: x =_A y$, then you shouldn't really think of $(x,y)$ as being "off the diagonal". Indeed, $p$ is a proof that $x$ and $y$ are equal... – Alex Kruckman Jun 29 '19 at 15:25
• Paraphrasing the HoTT book it is not the identity type $x=_Ay$ that is inductively defined, but instead the identity family $\sum_{x,y:A}x=_Ay$ is inductively defined by $\mathrm{refl}_x$, in the homotopy picture this is the free loop space over $A$, in which every loop is homotopic to a constant one – Alessandro Codenotti Jun 29 '19 at 16:04
• Specifically, you may find it helpful to read sections 1.12 and 2.1-2.3 of the HoTT Book, homotopytypetheory.org/book. – Mike Shulman Jun 29 '19 at 16:06
• As Alex points out, if $p: x=_A y$, then well $x$ and $y$ are equal. Homotopically, this is saying that the free path space $Map(I,A)$ is homotopy equivalent to $A$, more precisely it strongly deformation retracts onto $A$, which fits into it via constant paths. You can see $refl_x : x=_A x$ as the constant path in $A$, and $p:x=_A y$ as an arbitrary path. Then the induction principle tells us that since paths are homotopy equivalent to constant paths, we only need to define things on the latter. – Maxime Ramzi Jun 29 '19 at 21:59

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!).
• So given arbitrary $x,y:A$, $p: x =_{A} y$ and $f$ as in the question, how do we define the value of $B(x,y,p)$? Is it equal to $B(x,x,r(x))$ (and $B(y,y,r(y))$)? If so, specifically in which sense of equality? Also, isn't $\Pi_{x:A} B(a)$ the space of sections rather than fibers; or are these two viewpoints equivalent? – user Jul 1 '19 at 6:48
• @user That's the idea, but it is trickier than I made it look. Let's look a simpler dependent function for notational simplicity. If $p\colon x=_Ay$ and $f\colon \prod_{x\colon A} B(x)$ then a priori $f(x)\colon B(x)$ and $f(y)\colon B(y)$ don't even have the same type, so it makes no sense to ask whether they're equal! The idea here is that $p$ tells us how to build a function $p_\ast\colon B(x)\to B(y)$, which corresponds to transport in the homotopy picture and is explained in 2.3 of the HoTT book. (while fibers/sections was definitely a typo, thanks for catching it!) – Alessandro Codenotti Jul 1 '19 at 14:27