Categorical Intuition of Path Induction

Question

I am trying to understand path induction from the trinitarian point of view. So far I understand the informal intuition of path induction from a homotopical and computational point of view. But I am not sure how to think of path induction categorically. In the homotopical point of view, any path $p$ from $x$ to $y$ in a space $A$ can be continuously deformed into the constant path at $x$ by simply retracting the end point $y$ continuously along $p$. In the computational point of view, the path space is freely generated by the terms $refl x$ (or $id x$) for each $x$ in $A$.

However, thinking of types as $\infty$-groupoids, I'm not sure how to best justify path induction. Paths are supposed to be morphisms so that specifying a function $\prod_{x y : A}\prod_{p : x = y} C(x,y,p)$ is defining a function on the the path object (which is an $\infty$-groupoid) between any two points in $A$. The only thing that I can think of is a theorem from $1$-category that says every groupoid with at most one arrow in each homset is equivalent to a discrete category. Thus, specifying a function out of such groupoid is equivalent to specifying a function out of the discrete category. But this not a good way of thinking of things since path induction applies to arbitrary $\infty$-groupoids and so they need not be equivalent to some discrete $\infty$-groupoid.

Any explanations or references are appreciated.

Answer 1

Let me illustrate with 1-groupoids.

Given a 1-groupoid $A$ and two points (or objects or 0-cells, whatever you want to call them) $x$ and $y$ in $A$, the collection of paths (or morphisms or 1-cells) in $A$ between $x$ and $y$ is a set (or 0-groupoid), commonly denoted by $A (x, y)$. These sets are part of a larger structure, called the path fibration of $A$, consisting of a 1-groupoid $\textrm{Path} (A)$ and a functor $\textrm{Path} (A) \to A \times A$, defined as follows:

• The points in $\textrm{Path} (A)$ are the paths in $A$.

• The paths in $\textrm{Path} (A)$ are commutative squares in $A$.

• The functor $\textrm{Path} (A) \to A \times A$ sends each path in $A$, considered as a point in $\textrm{Path} (A)$, to its endpoints.

The fibre over $(x, y)$ is the set $A (x, y)$, but we could also look at the first projection $\textrm{Path} (A) \to A$ and ask about its fibres. It turns out that the fibre over $x$ is then the under-groupoid ${}^{x /} A$:

• The points in ${}^{x /} A$ are the paths in $A$ starting at $x$.

• The paths in ${}^{x /} A$ are commutative triangles in $A$.

There is a canonical point in ${}^{x /} A$, namely $\textrm{id}_x$, and it is easy to check that $\textrm{id}_x$ is an initial object in ${}^{x /} A$. But ${}^{x /} A$ is a 1-groupoid, so that means there is a unique path between any pair of points in ${}^{x /} A$, and thus ${}^{x /} A$ is contractible. The practical consequence of this is that to define a functor ${}^{x /} A \to B$, it is enough to say where $\textrm{id}_x$ goes to in $B$ – then we can just send every other point in ${}^{x /} A$ to the same point in $B$, and every path to the trivial path in $B$.

But this is exactly what path induction (well, recursion in this case) is telling you.

Answer 2

The point is that the $\infty-$groupoid $A(a,-)=\sum_{b:A} A(a,b)$ is trivial, for every $a$. Indeed, the projection $\pi$ to the trivial $\infty$-groupoid has an inverse $s$ mapping to the identity morphism of $a.$ An equivalence between $s\pi$ and the identity of $A(a,-)$ is given, at each $p:a\to b,$ by an inverse of $p.$ (Homotopically, this is the contractibility of based path spaces.) These equivalences fit together to an equivalence between $A$ and $\sum_{a,b} A(a,b)$, validating path induction.

Answer 3

I've always viewed the Yoneda lemma as "path induction for 1-categories".

It says that to specify a natural transformation $ \alpha \colon \mathrm{Hom}(-, c) \to F $, for $ F \colon \mathbf{C^{\mathrm{op}}} \to \mathbf{Set} $, you just have to specify what $ \alpha_c(\mathrm{id}_c) \in F(c) $ is, and the rest of the transformation naturally follows from the functoriality of $ F $ ($ \alpha_{c'}(f) $, for $ f \in \mathrm{Hom}(c', c) $, equals $ F(f)(\alpha_c(\mathrm{id}_c)) $).

In fact, motivated by this, I once formulated a "symmetric version" of the Yoneda lemma, which would correspond to path induction with both ends free: for every $ F \colon \mathbf{C}^{\mathrm{op}} \times \mathbf{C} \to \mathbf{Set} $, there is a natural bijection between natural transformations $ \alpha \colon \mathrm{Hom} \to F $ and extranatural transformations $ \beta \colon * \to F $, which are just tuples $ (\beta_c)_{c \in \mathbf{C}} \in \prod_{c \in \mathbf{C}} F(c, c) $ such that $ F(f, c')(\beta_{c'}) = F(c, f)(\beta_c) $ for every $ f \colon c \to c' $.

So perhaps a way to justify path induction is that to specify $ f \colon \prod_{x,y \colon A} \prod_{p \colon x = y} C(x, y, p) $, it's enough to say what every $ f(x, x, \mathrm{refl}_x) \colon C(x, x, \mathrm{refl}_x) $ is and the rest falls out of the functoriality of $ C $ (up to a higher equivalence)?