most recent 30 from http://mathoverflow.net 2013-05-20T19:01:45Z http://mathoverflow.net/feeds/question/103815 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/103815/intensional-equaity-in-type-theory Asymptotik 2012-08-02T19:53:07Z 2012-09-02T22:52:55Z

<p>Hi,</p> <p>I want to know why we add an intensional equality in type theory to definitional equality ? What is the aim with this intensional equality ?</p> <p>thanks</p>

http://mathoverflow.net/questions/103815/intensional-equaity-in-type-theory/106203#106203 kow 2012-09-02T22:52:55Z 2012-09-02T22:52:55Z

<p>The key thing to notice is that the definitional equality is a <em>judgement</em> and not a proposition (so in particular, definitional equalities can not be part of your assumptions, nor can they be proved, they can only be checked by the type-checker). The intensional equality, on the other hand, <em>is</em> a proposition, so it can be used as an assumption, and we can e.g. use induction to prove an intensional equality. </p> <p>The two equalities are closely connected, but do not generally agree: Martin-Löf's intensional type theory has decidable type checking, and hence also the definitional equality judgement is decidable, but you can convince yourself that the intensional equality is not decidable.</p> <p>Note that definitional equality entails intensional equality, but not the other way around.</p>