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.



Uniqueness principle for functions types in the HoTT book
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.


