move funext_from_interval to IntervalImpliesFunext, not exported by HoTT

Do we not import UnivalenceImpliesFunext?