Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the domain, then $f = g$) is not an axiom in the standard constructive logic of Coq. Of course, one can add it as an axiom in one's files, but it is not obviously available in any pre-defined tactics. I am left wondering...

**1.** What is the thinking behind considering function extensionality as foreign to the calculus of constructions? I thought that from a computational perspective, a function really *is* there to be applied to things, and cannot carry any more information than what it does to them (and its type). For a moment I suspected that Coq avoids function extensionality in order to allow applying results to models like arbitrary enriched categories whose internal homomorphisms carry some more information than plain morphisms. But this is not the case: Coq (since version 8.4) has a implementation of eta-expansion (saying that any function $f$ equals the function sending every $x$ in its domain to $f\left(x\right)$, provided the types are right). In an enriched category, this would pour any additional structure of an internal Hom down the drain. (I must say the eta-expansion in Coq feels rather weird, too -- it is triggered by the `reflexivity`

tactic. I expected it to be a tactic on its own...) Having eta-expansion but no extensionality is seriously confusing: one can have $f\left(x\right) = g\left(x\right)$ for all $x$, and yet one cannot rewrite the $f\left(x\right)$ in "the function sending every $x$ to $f\left(x\right)$" as a $g\left(x\right)$. And there I thought the bound variable in a lambda term would be like the bound variable in a forall quantification?

**2.** On a more practical note (and more on-topic in MathOverflow), how much do the axiom of function extensionality and the (weaker) axiom of eta-expansion contribute to the strength of the logic? (At this point I have to admit that I don't really know the definition of the logic involved, so I'll just say I'm talking about the logic of Coq with no additional axioms assumed; it has so far been agreeing with my intuitive understanding of constructivism, until extensionality came along.) If I can define two terms $a$ and $b$ of type $\mathrm{nat}$ (natural numbers) and use function extensionality (resp. eta-reduction, both ways) to prove their equality, can I also do it without? If I can prove a (more complicated) statement using function extensionality, is there a way to transform it into a (possibly clumsier) statement which can be proven without function extensionality and which can be transformed into the former statement using some straightforward applications of function extensionality?

I'm sorry for logical naivety. The way I am posing the question, I fear it would qualify as soft; nevertheless I am pretty sure that there is some precise statements to be made here (or maybe just a reference to a textbook to be given).

5more comments