Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
identity_type [2016/04/12 15:40] nikolaj |
identity_type [2016/07/20 01:23] nikolaj |
||
|---|---|---|---|
| Line 16: | Line 16: | ||
| | ${\large\frac{\dots,\,p\,:\,Id_A(x,y)\ \vdash\ Q(x,y,p)\,:\,\mathrm{Type}\hspace{.5cm}\dots\ \vdash\ t\,:\,Q(x,x,refl_x)}{\dots\ \vdash\ J(t,x,y,p)\,:\,Q(x,y,p)}}$ | | | ${\large\frac{\dots,\,p\,:\,Id_A(x,y)\ \vdash\ Q(x,y,p)\,:\,\mathrm{Type}\hspace{.5cm}\dots\ \vdash\ t\,:\,Q(x,x,refl_x)}{\dots\ \vdash\ J(t,x,y,p)\,:\,Q(x,y,p)}}$ | | ||
| - | This means that is we know that $x=y$, then if $Q(x,x)$ is true, then so must be $Q(x,y)$. | + | This means that if we know that $x=y$, then if $Q(x,x)$ is true, then so must be $Q(x,y)$. |
| == Computational rule == | == Computational rule == | ||
| Line 73: | Line 73: | ||
| ==== Intension, extension ==== | ==== Intension, extension ==== | ||
| + | See [[http://mathoverflow.net/questions/156238/function-extensionality-does-it-make-a-difference-why-would-one-keep-it-out-of | ||
| + | | Andrej Bauer on intentional equality]] | ||
| + | |||
| === The concept === | === The concept === | ||
| There is a correspondence between a predicate $P$ over a class of objects and it's //extension// $\{x\ |\ P(x)\}$. The latter is the collection of objects it describes. | There is a correspondence between a predicate $P$ over a class of objects and it's //extension// $\{x\ |\ P(x)\}$. The latter is the collection of objects it describes. | ||
| Line 80: | Line 83: | ||
| We see that intensionally different definition can have the same extension. | We see that intensionally different definition can have the same extension. | ||
| - | Another remark: | + | == Canonical form, canonicity of formal systenms)== |
| We have $2(12+15)=2*3*4+2*3*5=3(8+10)$, and while $2(12+15)\mapsto 24+30$ and $3(8+10)\mapsto 24+30$ feel like natural reductions, $2(12+15)\mapsto 3(8+10)$ feels random. That is to say, there is a sort of computational direction that comes with a formulized evaluation. | We have $2(12+15)=2*3*4+2*3*5=3(8+10)$, and while $2(12+15)\mapsto 24+30$ and $3(8+10)\mapsto 24+30$ feel like natural reductions, $2(12+15)\mapsto 3(8+10)$ feels random. That is to say, there is a sort of computational direction that comes with a formulized evaluation. | ||
| + | |||
| + | nLab: | ||
| + | [[https://ncatlab.org/nlab/show/canonical+form | canonical form]] | ||
| === In theories === | === In theories === | ||
| Line 101: | Line 108: | ||
| === Reference === | === Reference === | ||
| - | nLab: [[http://ncatlab.org/nlab/show/identity+type|identity type]] | + | nLab: |
| + | [[http://ncatlab.org/nlab/show/identity+type|identity type]] | ||
| + | [[https://ncatlab.org/nlab/show/canonical+form | canonical form]] | ||
| + | |||
| + | |||
| + | StackExchange: | ||
| + | [[http://mathoverflow.net/questions/156238/function-extensionality-does-it-make-a-difference-why-would-one-keep-it-out-of | ||
| + | | Andrej Bauer on intentional equality]] | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Related === | === Related === | ||
| [[Dependent type theory]] | [[Dependent type theory]] | ||
