Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Last revision Both sides next revision
babbys_first_hott [2015/08/02 20:46]
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.
Link to graph
Log In
Improvements of the human condition