Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
identity_type [2016/04/12 15:42] nikolaj |
identity_type [2016/04/12 15:53] nikolaj |
||
---|---|---|---|
Line 83: | 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 106: | Line 110: | ||
nLab: | nLab: | ||
[[http://ncatlab.org/nlab/show/identity+type|identity type]] | [[http://ncatlab.org/nlab/show/identity+type|identity type]] | ||
+ | [[https://ncatlab.org/nlab/show/canonical+form | canonical form]] | ||
+ | |||
StackExchange: | StackExchange: |