Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
babbys_first_hott [2015/08/02 20:46] nikolaj |
babbys_first_hott [2017/03/13 00:13] nikolaj |
||
|---|---|---|---|
| Line 45: | Line 45: | ||
| $Semigroup\equiv{\large{\sum}}_{A:\mathrm{Type}}{\large{\sum}}_{m:A\to A\to A}{\large{\prod}}_{x:A}{\large{\prod}}_{y:A}{\large{\prod}}_{z:A}\ m(x,m(y,z))=_A m(m(x,y),z)$ | $Semigroup\equiv{\large{\sum}}_{A:\mathrm{Type}}{\large{\sum}}_{m:A\to A\to A}{\large{\prod}}_{x:A}{\large{\prod}}_{y:A}{\large{\prod}}_{z:A}\ m(x,m(y,z))=_A m(m(x,y),z)$ | ||
| - | A term of $SemiGroupStr$ is a pair $\langle A,\langle m,p\rangle\rangle$, where the first entry is a type $A$ and the second entry is pair, where the first entry is a function $m:A\to A\to A$ and the second entry is a proof $p$ that this this $m$ fulfills the usual axiom. We do constructive mathematics here, so $p$ is a function which takes any $x$ to a function which takes any $y$ to a ... to a function which takes any $m(m(x,y),z)$ to a term which demonstrates the required equality. | + | A term of $SemiGroupStr$ is a pair $\langle A,\langle m,p\rangle\rangle$, where the first entry is a type $A$ and the second entry is pair, where the first entry is a function $m:A\to A\to A$ and the second entry is a proof $p$ that this $m$ fulfills the usual axiom. We do constructive mathematics here, so $p$ is a function which takes any $x$ to a function which takes any $y$ to a ... to a function which takes any $m(m(x,y),z)$ to a term which demonstrates the required equality. |
| == Example 2 == | == Example 2 == | ||
| 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. | ||
