4
$\begingroup$

Chapter 1.2 of the HoTT book says this about eta-conversion:

$$ f \equiv (\lambda x . f(x)). $$ This equality is the uniqueness principle for function types, because it shows that $f$ is uniquely determined by its values.

That "$f$ is uniquely determined by its values" seems like a stronger property than eta-equivalence. Or perhaps I'm just not sure how to interpret that particular phrase. To me, that phrase seems to describe an extensional equivalence principle for functions, which is different from eta-conversion as far as my understanding goes.

So I suppose my actual question is: what are the "values" of $f$? I would think the "values" of $f$ would be its image. But that leads to a nonsensical reading of this phrase, which leads me to think the "values" of $f$ refers to how $f$ acts on its inputs. But then we would have functional extensionality, and I'm pretty sure that's not what this sentence is trying to say. (Or is it?)

For example, I would not expect $\lambda x . x + 3$ to be definitionally equal to $\lambda x . 3 + x$. But for any meaning for the "values" of these two functions as far as I can imagine, this sentence from the book would imply that these functions are (definitionally) equal.

Or maybe "values" refers to irreducible terms according to the operational semantics?

Perhaps I am reading too much into the wording of the sentence? As far as I know, I understand what the equality means. I'm just confused about the exposition that directly follows it and want to make sure I'm not missing anything.

$\endgroup$
  • 1
    $\begingroup$ They mean that f is defined up to definitional equality by how it acts on inputs in the sense of knowing its inputs up to definitional equalty. However you should be aware that this is not a proposition in the sense "if f(a) is definitionally equal to g(a) for all a, then f and g are definitionally equal" (which would not make sense). The only reasonable way to make it precise is the given judgement that f is equal to the lambda term defined by it. You can call this function extensionality, though hott also has propositional function extensionality. $\endgroup$ – Jakob Werner Nov 17 at 10:55
  • 3
    $\begingroup$ The confusion about your example is because x+3 and 3+x are not equal by definition. $\endgroup$ – Jakob Werner Nov 17 at 10:56
  • $\begingroup$ Aha! I was thinking too computationally. For some reason I was associating the "values" of f with normal forms of closed terms. I believe this clears up my confusion. Thank you! $\endgroup$ – stovetop Nov 17 at 11:23
  • 1
    $\begingroup$ I suggest you also carry out what I believe is the first exercise of chapter 1, namely showing that (hg)f is equal by definition to h(gf), because they act the same way on elements. A precise proof will be using the uniqueness principle. $\endgroup$ – Jakob Werner Nov 17 at 11:35
7
$\begingroup$

It is less confusing to first see how things work for ordered pairs. Consider the following two rules:

  1. $\eta$-equality for pairs: $$\frac{u : A\times B}{u \equiv (\pi_1 u, \pi_2 u)}$$
  2. extensionality rule for pairs: $$\frac{v : A\times B \quad w : A\times B \quad \pi_1 v \equiv \pi_1 w \quad \pi_2 v = \pi_2 w}{v \equiv w}$$

(Note: it is important that we consider rules, which are not to be confused with corresponding inhabitants of certain types, e.g. $\Pi (u : A \times B) \,.\, \mathrm{Id}_{A \times B}(u, (\pi_1 u, \pi_2 u))$.)

There are several ways in which we can read the above rules. The $\eta$-rule states that an element of $A \times B$ does not change if we take it apart and put it back together. It also states that every element of $A \times B$ is (equal to) a pair, namely the one we get by pairing together its components. Extensionality states that elements of $A \times B$ are equal if their projections are equal.

But these two principles are inter-derivable in the presence of congruence rules and $\beta$-rules for pairs:

  • $\eta$-rule implies extensionality: if $\pi_1 v = \pi_1 w$ and $\pi_2 v = \pi_2 w$ then by the $\eta$-rule $v = (\pi_1 v, \pi_2 v) = (\pi_1 w, \pi_2 w) = w$.

  • extensionality implies the $\eta$-rule: because $\pi_1 u = \pi_1 (\pi_1 u, \pi_2 u)$ and $\pi_2 u = \pi_2 (\pi_1 u, \pi_2 u)$, by extensionality $u = (\pi_1 u, \pi_2 u)$.

Let us repeat the exercise for function types, but first we should clear up what is meant for a function to "have a value". An ordered pair does not just "have components" -- it has a first component and a second component. Likewise, a function $f : A \to B$ does not just "have values" -- it has a value at an argument. We may extract the value at $a : A$ by applying $f$ to $a$.

Here are the $\eta$-equality and extensionality rules for functions:

  1. $\eta$-equality for functions: $$\frac{f : A \to B}{f \equiv (\lambda x \colon A \,.\, f\, x)}$$
  2. extensionality rule functions: $$\frac{f : A \to B \quad g : A \to B \quad x : A \vdash f \, x \equiv g \, x}{f \equiv g}$$

(Note: at this point it is really quite important not to confuse the above function extensionality rule with what is known as function extensionality axiom, which states that $\Pi (f, g : A \to B) \,.\, (\Pi (x : A) \,.\, \mathrm{Id}_B(f x, g x)) \to \mathrm{Id}_{A \to B}(f, g)$ is inhabited.)

The situation is essentially the same as before. The $\eta$-rule states that a function does not change if we apply it to a variable and then abstract over the variable. It also says that every element of $f : A \to B$ is a function, namely the one that maps $x$ to $f \, x$. The extensionality rule says that two elements of $A \to B$ are equal if they act the same way on arguments. Another way to say this is: if $f$ and $g$ have equal values (at an arbitrary argument $x : A$), then they are equal.

I will leave it as an exercise to show that the $\eta$-equality and extensionality rules for functions are inter-derivable.

But can we read the $\eta$-rule as stating that "$f$ is determined by its values"? Yes of course: $f$ is equal to the mapping which takes an argument $x : A$ to $f \, x$ (the value of $f$ at $x$).

I hope these considerations make it clear in what sense the $\eta$-equality rule for functions states that a function is determined by its values.

P.S.: In your question you suggest an interpretation by which "have the same values" means "have the same image". This is quite nonsensical, as it matters which arguments maps to any given value in the image. After all $\sin$ and $\cos$ have the same image $[-1,1]$ but they're hardly equal.

$\endgroup$
  • $\begingroup$ I don't understand this: "It also says that every element of $f:A\to B$ is a function, namely the one that maps $x$ to $f(x)$.". I assume you meant "every element $f:A\to B$ is a function, namely the one that maps $x$ to $f(x)$." But aren't all element of $A\to B$ called functions by definition? Or put differently: if we don't have eta, would there be a reason not to call all elements of $A\to B$ functions? $\endgroup$ – Michael Bächtold Nov 17 at 21:11
  • $\begingroup$ I would say that by definition a function is something that manifestly maps arguments to values, such as a $\lambda$-abstraction. What if $A \to B$ contains something that cannot be shown to be of this form? What if it contains an animal with long ears that hops around, would you still call it a "function"? Luckily, the $\eta$-rule prevents this possibility. $\endgroup$ – Andrej Bauer Nov 17 at 22:23
  • 1
    $\begingroup$ Again, in OCaml you can write (raise Not_found) 5 to apply raise Not_found to an argument, yet nobody would argue (I hope) that raise Not_found is a function. The elimination rule for functions in OCaml is standard. So I disagree. The thing which tells us that every element of $A \to B$ is a function is precisely the $\eta$-rule, which in fact fails in a typical programming language. $\endgroup$ – Andrej Bauer Nov 18 at 6:32
  • 1
    $\begingroup$ Another consideration: a weak exponential in a category need not satisfy the $\eta$-rule but it satisfies the elimination rule. And when we look at examples of weak exponentials, we see that their elements are representations of functions, i.e., entities that hold enough information so that they can be applied. However, they may hold too much information in the sense that they are not determined by their values. $\endgroup$ – Andrej Bauer Nov 18 at 6:35
  • 1
    $\begingroup$ They are not the same. Define let rec h x = h x. The program try f with _ -> h () terminates but try (raise Not_found) with _ -> h () cycles forever. The only difference between the two is f versus raise Not_found. $\endgroup$ – Andrej Bauer Nov 18 at 20:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.