Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
babbys_first_hott [2015/02/06 13:58] nikolaj |
babbys_first_hott [2016/07/18 01:14] nikolaj |
||
|---|---|---|---|
| Line 82: | Line 82: | ||
| For any $n,m$, the above identity type $n=_\mathbb{N}m$ is defined in a way so that its either ${\bf 0}$ or ${\bf 1}$. So it either has a term or not, and under Curry-Howard the former means it's false and the latter means it's true. The dependent type $=_\mathbb{N}$ is equivalent to a binary predicate or a function of type $\mathbb N\to\mathbb N\to\mathbb {\bf 2}$ but to consider it a map into $\mathrm{Type}$ becomes important in the following. | For any $n,m$, the above identity type $n=_\mathbb{N}m$ is defined in a way so that its either ${\bf 0}$ or ${\bf 1}$. So it either has a term or not, and under Curry-Howard the former means it's false and the latter means it's true. The dependent type $=_\mathbb{N}$ is equivalent to a binary predicate or a function of type $\mathbb N\to\mathbb N\to\mathbb {\bf 2}$ but to consider it a map into $\mathrm{Type}$ becomes important in the following. | ||
| - | There are a million ways to define and work with equality. For example, depending on the theory you treats functions intentional or extenional, the function mapping $n$ to $2(n+5)$ and the function mapping $n$ to $2n+10$ might be judged to be different or the same. For example, the former theory might be suited to study the difference between sorting algorithms (which do the same job, but possibly need different number of computing steps), while the latter may not. Intensional theories also have better decidablity properties regarding type checking but, as one can remember, they are also much more complicated to work with. | + | There are a million ways to define and work with equality. For example, depending on the theory you treats functions intentional or extenional, the function mapping $n$ to $2(n+5)$ and the function mapping $n$ to $2n+10$ might be judged to be different or the same. For example, the former theory might be suited to study the difference between sorting algorithms (which do the same job, but possibly need different number of computing steps), while the latter may not. Intensional theories also have better decidablity properties regarding type checking but, as one can imagine, they are also much more complicated to work with. |
| We now turn to a variation of intentional type theory with an additional axiom which implies function extensionality. | We now turn to a variation of intentional type theory with an additional axiom which implies function extensionality. | ||
| Line 98: | Line 98: | ||
| {{ thed.jpg?X400}} | {{ thed.jpg?X400}} | ||
| - | We can inductively define the circle $\mathbb S$ as type by postulating | + | We can inductively define the circle $\mathbb S$ as type by postulating |
| $base:\mathbb S$ | $base:\mathbb S$ | ||
| - | |||
| and | and | ||
| - | |||
| $loop:base=_{\mathbb S}base$. | $loop:base=_{\mathbb S}base$. | ||
| - | |||
| Now | Now | ||
| - | |||
| $\dots,loop^{-2},loop^{-1},refl_{base},loop,loop^2,loop^3,\dots$ | $\dots,loop^{-2},loop^{-1},refl_{base},loop,loop^2,loop^3,\dots$ | ||
| - | |||
| are all terms of $base=_{\mathbb S}base$. | are all terms of $base=_{\mathbb S}base$. | ||
| This type can be shown to be equivalent (in the formal sense discussed below) to the integers. Indeed, recall that the first homotopy group of the circle is isomorphic to $\mathbb Z$. | This type can be shown to be equivalent (in the formal sense discussed below) to the integers. Indeed, recall that the first homotopy group of the circle is isomorphic to $\mathbb Z$. | ||
| Line 128: | Line 122: | ||
| $isSet(A):={\large{\prod}}_{x:A}{\large{\prod}}_{y:A}\,isProp(x=y)$ | $isSet(A):={\large{\prod}}_{x:A}{\large{\prod}}_{y:A}\,isProp(x=y)$ | ||
| - | The above says that $x$ connects to $y$ via at most one invertible path and hence this characterizes as set as a discrete category. Since sense, characterized like here as types with lack of other structure, are generally different from sets characterized in a theory like ZFC. | + | The above says that $x$ connects to $y$ via at most one invertible path and hence this characterizes as set as a discrete category. Since sets, characterized like here as types with lack of other structure, are generally different from sets characterized in a theory like ZFC. |
| == Homotopy theory == | == Homotopy theory == | ||
