First of all: Hello everyone! Thanks for the great work on the nLab. So far it was a joy to absorb a lot, but today I shall actively engage in the discussion for the first time.

On the page about equality in the section about definitional equality the following is said:
“The most basic one is **definitional equality or intensional equality**. … “

As well as:
“For instance the symbols “2” and “s(s(0))” (meaning the successor of the successor of 0) are **definitionally/extensionally** equal terms (of type the natural numbers):”

Can both these statements be true? If so, I think this is a bit confusing and some clarification would be great.

Edit: Inserted Toby’s link syntax hint.

]]>Just wondering if there are relatively simple reasons why good computational qualities, like decidable type and equality checking, fail in extensional type theory. I’m just beginning to read some of this homotopy type theory stuff, but am relatively familiar with at least the bare bones of type theory. Is there some intuitive reason behind this, or is it sort of a technical result?

]]>