function extensionality

[DanGrayson]

I'm a little dissatisfied with this discussion:

because, a priori, there may be multiple functions of type ( ∏ (x:X), ( f(x) = g(x) )) → f=g.

[marcbezem]

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

[DanGrayson]

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.

[marcbezem]

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".

[DanGrayson]

What about this way of putting it?:

[marcbezem]

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.

[marcbezem]

Done 03739c1

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