Question

Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that:

Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the things one wants to do... certain theorems simply do not hold due to the lack of extensionality. A typical example is that from $t\in B a$ and $p\in Id A ab$ one is not allowed t conclude that $t\in Bb$ where $A$ is a type and $B$ is a family of types indexed over $A$.(But of course one is allowed to infer $t\in Bb$ from $t\in Ba$ and $a=b\in A$ !)

An almost similar thin is mentioned in Definition of extensional and propositional equality in Martin-Lof extensional type theory :

The (Id-DefEq) means that extensional equality is baked into the type system: if you have a type constructor 𝑇:((𝑥:𝑈)→𝑉)→𝖲𝖾𝗍 then you can use a value of type 𝑇 𝑓 in a context expecting 𝑇 𝑔 if 𝑓 and 𝑔 map equal inputs to equal outputs. Again this is not true in an intensional system, where 𝑓 and 𝑔 might be incompatible if they're syntactically different.

Why is that? Isn't it that two functions that are producing exactly same output for their inputs, equal? So why can't one be replaced with another in a context? What makes definitionally equal functions eligible to be replaced with each other, but not the extensionally equal ones?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top