The "homotopic"/Geometric Nature of Mathematical Induction

 Mathematical Induction for the Natural Numbers ${\mathbb N}$ can be expressed as the following Inference rule within Martin-Löf's Dependent Type Theory:

$\Gamma\,,\,x:{\mathbb N}\,\vdash\,P(x)\;Type$

$\Gamma \,\vdash\,p_0\,:\,P(0_{\mathbb N})$

$\Gamma \,\vdash\,p_s\,:\,\Pi_{(n:{\mathbb N})}\,P(n)\,\to\,P(succ_{\mathbb N}(n))$

 $-----------------\;{\mathbb N} ind$ 

$\Gamma \,\vdash\, ind_{\mathbb N}(p_0\,p_s) \,:\, \Pi_{(n:{\mathbb N})}\,P(n)$

with the computation rules -where we implicitly assume the same premises:

$ind_{\mathbb N}(p_0\,,\,p_s\,,\,0_{\mathbb N})\,\doteq\,p_0\,:\,P(0_{\mathbb N})$

$ind_{\mathbb N}(p_0\,,\,p_s\,,\, succ(n) ) \,\doteq\, p_s(n\, ,\, ind_{\mathbb N}(p_0\,,\,p_s\,,\, n )) \,:\, P(succ(n))$

Together this can be expressed graphically as  

 Thus, induction provides a way to build a function for free on an Inductive Type: If we have a way to hop from one fiber to "its neighboring" fiber, then, given a point at a starting fiber, we can built a section in the total space of that Type.  

That way of "hopping" between fibers is nothing else than the inductive step! 

First analogy, a curve can be defined by a differential equation and an initial condition. This equation can be given by a vector field that expresses the tangent to the curve at each point.

Also, in Differential Geometry we have the Covariant derivative, which expresses how we can move a tensor between infinitesimally close points in order to compare it meaningfully at those two points. Imposing the "Covariant change" to be zero along a given curve gives us a particular way to move a tensor between infinitesimally close points such that it stays parallel. This is the parallel transport of a tensor.

We can do the following: parallel transport a vector field along the very same curve it defines.  This curve is nothing other than a geodesic.

I'm definitely tempted to draw here an analogy between these Differential Geometry problems and the Induction rule, I'm just not sure what the best analogy might be. As induction gives as a curve, is Induction akin to building a geodesic through a point?

More general an analogy is the relation between induction an Sheaf theory. Paraphrasing an LLM, "both guarantee existence of global objects from local rules, though the technical frameworks differ: induction is sequential and algebraic; sheaf theory is topological and categorical".

Analogies aside, Dependent Type Theory through the lens of Homotopy Type Theory is very rich in intuitive pictures. I find this super cool!

The Curry-Howard Correspondence

 Logic, from the point of view of Dependent Type Theory (DTT), hinges on the Curry-Howard interpretation/correspondence:

Any proposition/predicate is a Dependent Type (DT)

Take the following statement about the Natural numbers $\mathbb N$: $d\,\vert\,n\;\equiv$ "d divides n"

As we know from classical Number Theory, this is equivalent to saying (classical logic) $\exists\, k\,\in\,{\mathbb N}\;\vert\quad d\cdot k\,=\,n$.

Hence, the correspondence is 

$d\, \vert\, n\quad\leftrightarrow\quad\Sigma_{(k:\mathbb N)}d\cdot k\;=\;n$

On the LHS we have classical Logic/Number Theory; on the RHS we have Dependent Type Theory. Thus, in DTT the existential quantifier gets translated into a dependent sum.

But what is that equality on the rhs? Ans.: $IdentPath_{\mathbb N}(d\cdot k\,,\,n)$, the Path type defined on the Natural numbers identifying both values.

Thus, any value $p$ of that sum type, $p\,:\,\Sigma_{k:\mathbb N}d\cdot k = n$, is a point $\left(k\, ,IdentPath_{\mathbb N}(d\cdot k\, , n)\right)$ that provides a proof of the divisibility of $n$ by $d$.

Let's see how we would prove a statement like "any natural numbers $x$ is divisible by 1". The universal quantifier from classical logic involved here gets translated into the Product type:

$\Pi_{x:\mathbb N }\,1\vert x\quad\equiv\quad\Pi_{x:\mathbb N}\Sigma_{k:\mathbb N}\,1\cdot k = x$

In oder to prove this we need to find/construct a "witness" or element $p\,:\,\Pi_{x:\mathbb N}1\vert x$. Incidentally, this is called a section on the space $\Sigma_{x:\mathbb N}1\vert x$.

Decomposing $p$ by applying it to a number $x$ we see that it must be $p(x):\Sigma_{k:\mathbb N}1\cdot k = x$. Again, this is of the form $(k, q(x))$, where $q(x):\,1\cdot k\,=\,x$.

Here comes where would use the fact that in a DTT formulation of the Natural Numbers we would previously have constructed a path like $r(x)\,:\,1\cdot x\,=\,x$, which corresponds to the rule of left multiplication by the neutral element of the product in the Natural numbers. 

Hence, we have the element $p(x) = \left(x\, ,r(x)\right)$ which is of the desired type $\Sigma_{k:\mathbb N}1\cdot k\,=\,x$. As $x$ is an arbitrary number,  $p$ is the sought for function $p\,:\,\Pi_{x:\mathbb N}\,1\vert x$.  

We have thus proved in Dependent Type Theory that 1 divides any natural number.

I thought these two examples could show the gist of how to think in Dependent Type Theory about logical problems and proofs. 

Andrej Bauer's online course slides are great, but one of the books he recommends for further reading I'm starting to like quite a lot:   "Introduction to Homotopy Type Theory" by Egbert Rijke, which is available for free at https://arxiv.org/pdf/2212.11082. These examples are from there.