function extensionality about symmetrybook HOT 6 CLOSED

Yes, we discussed that and that's why you called it a principle and not an axiom.

from symmetrybook.

It might be better to move it to the section on equivalences, so we could take that function to be an inverse of the function in the exercise.

from symmetrybook.

The narrative I tried to follow is: if I introduce a type former, here X->Y, I explain what it "means" that to elements of the newly formed type are equal in terms of equality of the constituent types. This "means" is often modulo an equivalence, and cannot be made precise before the definition of equivalence is in place. Cf. "equivalent" in the last sentence of 5.3.
This narrative makes sense to me, and we discussed this a couple of times. Do you really want to change that? Or only in case of function extensionality? A good solution could be to add a short section in between 2.8 and 2.9, called "Identifying functions".

from symmetrybook.

What about this way of putting it?:

from symmetrybook.

Fine with me. But we could give a name to the function in Exc. 2.4.3 and come back to this when we have equivalences. I can make a proposal.

from symmetrybook.

Done 03739c1

The exercise had to become a definition since we cannot have an axiom depend on how somebody solves the exercise.

from symmetrybook.