Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
identity_type [2016/04/12 15:40] nikolaj |
identity_type [2016/04/12 15:42] nikolaj |
||
|---|---|---|---|
| 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 101: | Line 104: | ||
| === Reference === | === Reference === | ||
| - | nLab: [[http://ncatlab.org/nlab/show/identity+type|identity type]] | + | nLab: |
| + | [[http://ncatlab.org/nlab/show/identity+type|identity type]] | ||
| + | |||
| + | 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]] | ||
