# Has extensionality ever caused any problems in a mathematical proof?

Agda does not presume extensionality, but we can postulate that it holds:

postulate
extensionality : ∀ {A B : Set} {f g : A → B}
→ (∀ (x : A) → f x ≡ g x)
-----------------------
→ f ≡ g


Postulating extensionality does not lead to difficulties, as it is known to be consistent with the theory that underlies Agda.

More generally (and before using it everywhere), I wanted to check if it's always safe to use in proving (constructive) mathematics. Or is it just OK with Agda, but not with some other proof assistants.

Has extensionality caused any known problems in proofs of constructive mathematics?

• What do you mean by "safe" and what do you mean by "constructive mathematics"? Commented Mar 19 at 9:08
• @AndrejBauer By constructive mathematics, I mean those without LEM. That's about what I know for constructive math. For safe, I mean not leading to a wrong answer if done on paper and pencil. Commented Mar 19 at 9:26

Function extensionality is “safe“ in the sense that it is valid in traditional constructive mathematics, for example as practiced by Erret Bishop, as well as in any topos. It is also valid in homotopy type theory, because it is a consequence of the Univalence axiom.

Function extensionality is a very natural principle to adopt from a mathematical point of view. It is quite difficult to develop ordinary mathematics (classical or constructive, it does not matter), without good extensionality princoples – not just for functions but also for other constructions.

There are situations in which one needs to pay attention, however. If we are working in type theory that does not validate function extensionality (Martin-Löf type theory, Agda, Coq) then we might be tempted to postulate it as an axiom, because it is still ”safe” in the sense that it does not lead to any contradictions. However, doing so may ruin good computational behavior of the underlying calculus. For example, if we postulate extensionality in Agda, then it is not true anymore that every closed term of type nat normalizes to a numeral. Here is an example:

open import Data.Nat
open import Data.Unit
open import Relation.Binary.PropositionalEquality

postulate
extensionality : ∀ {A B : Set} {f g : A → B}
→ (∀ (x : A) → f x ≡ g x)
-----------------------
→ f ≡ g

not-a-numeral : ℕ
not-a-numeral = subst (λ (_ : ⊤ → ⊤) → ℕ) (extensionality λ _ → refl) 42


So, if you care about computation with proof terms, you might think twice before postulating anything. And even if you do not, having to deal with badly normalizing terms is still going to be a pain.

• Thanks a lot. Could you provide some references/tutorials on these "computational behavior" aspects? I tried your code and not-a-numeral indeed does not normalize. But I am not familiar with the theory about why/when such happens. Commented Mar 19 at 10:24
• There is one computation rule for subst, namely subst P refl x ≡ x and because in the given example extensionality λ _ → refl is not equal to refl, the rule cannot be used. So not-a-numeral does not compute. Commented Mar 19 at 10:43

Kind of fun to note that extensionality is inconsistent with the internal Church Thesis which states that every function $$\mathbb{N}\rightarrow\mathbb{N}$$ is realized by some Turing machine.

In turn Church's Thesis is consistent in systems like Coq or Agda.

By popular demand, let me expand on this. I'm referring to a lemma like in this Coq code, which states

$$\mathrm{CT}_\Sigma\ \mathrm{and}\ \mathrm{Ext}\Rightarrow\bot$$

with $$\mathrm{Ext}$$ being the principle of extensionality as you've stated it, and $$\mathrm{CT}_\Sigma$$ being the computational Church-Turing thesis, which states that the type

$$\prod_{f:\mathbb{N}\rightarrow\mathbb{N}}\{n : \mathbb{N}\mid n\ \mathrm{computes}\ f\}$$

is inhabited (and $$\mathrm{computes}$$ is the boring old definition of "is a code for a total Turing-machine that computes $$f$$")

This is actually a quite strong statement, so perhaps the surprising thing is that it's consistent at all! This isn't obvious, and one would typically prove it by giving a realizability interpretation that has a buit-in quote operator which extracts the code from a term. I think Andrej is the expert here.

It's pretty easy to jiggle things a bit and get inconsistency though, and if function extensionality is present, this can simply be done by

1. Proving that there is no Turing machine that decides whether a given p.r. function is equal to $$\lambda x:\mathbb{N}. 0$$
2. Using $$\mathrm{CT}_\Sigma$$ to build exactly such a function, by seeing if the code of a function is equal to that of $$\lambda x.0$$.

This was all taken from Forster's excellent survey Church’s Thesis and Related Axioms in Coq’s Type Theory.

It's worth noting that a similar axiom, $$\mathrm{CT}$$, which inhabits

$$\forall f:\mathbb{N}\rightarrow \mathbb{N}\ \exists n \mbox{ s.t. } n\ \mathrm{computes}\ f$$

in the Coq $$\mathrm{Prop}$$ universe (which does not allow computing elements of, say, $$\mathbb{N}$$) does not seem to be in contradiction with $$\mathrm{Ext}$$. I'm not sure how one would go about proving this though (but see the comments).

• I'm confused, the paper says that univalence is consistent with CT but that funext is not, but univalence implies funext? Commented Mar 20 at 5:23
• It is inconsistent if by "some" you mean Σ and not ∃; see lemma 29 in the paper. The ∃ version is consistent with univalence, and hence function extensionality. Commented Mar 20 at 8:45
• An the strong version of CT with a Σ has been shown recently to be consistent with MLTT (and the proof should probably scale to most additional features of Coq/Agda) Commented Mar 20 at 9:42
• It would be helpful if the answer explained more carefully what is going on. As written, it is perhaps entertaining but also misleading or confusing. What the precise conditions under which CT is inconsistent with function extensionality? Please don't just refer to some lemma in some paper, a short summary ought to be possible. Commented Mar 20 at 11:36
• Under one interpretation, namely the internal laguage of the effective topos, Church's thesis (as formulated in the literature using first-order logic and Kleene's $T$ and $U$) is consistent with function extensionality. This is a good reason why the answer requires clarification. Commented Mar 20 at 11:38