And the last one of this thread on my historical questions to Vladimir in 
2015:


On Oct 22, 2015, at 4:50 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

One more question, if you don't mind, this time technical: what made
you conjecture that univalence implies function extensionality, before
you had a proof? This is a very interesting thought.


No, it was almost an accident. I started a new file in Foundations that was 
supposed to contain results that depend on the UA and then I guess I 
started to think whether the UA and function extensionality are independent 
and came up with a proof of UA => FA. 

I think it was a turning point since  this is were constructivists got 
really interested in the UA (and UF).

Vladimir

>
>