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.