On Wednesday, 6 February 2019 05:13:35 UTC+1, Anders Mörtberg wrote:
Consider the interval HIT, it is contractible and hence equivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Unit type.
I have the feeling that function extensionality is special in the sense that the proof that I know of, as well as that of function extensionality in ETT, relies on the fact that we can replace judgmentally equal terms under lambdas, which is like function extensionality for judgmental equality.