Prove that the interval type 𝕀 with strict β-laws on point constructors implies function extensionality

[fredrik-bakke]

A possible approach to proving this fact is to first prove that the interval type $𝕀$ (defined in synthetic-homotopy-theory.interval-type) is a representing object for identifications, i.e. $$A^𝕀 \simeq \sum_{(x,y:A)}(x=_Ay)$$ for all types $A$, and then use that it gives us a type to curry over, hence "pulling the identification out of the Π" by an equivalence. The currying equivalence is equiv-swap-Π in foundation.type-arithmetic-dependent-function-types.

The resulting proof should probably be named funext-𝕀 and be placed in a new section of synthetic-homotopy-theory.interval-type. Caution should be made not to accidentally invoke function extensionality somewhere in the proof by applying a lemma that relies on it.

For a reference, this fact is partially established in the HoTT book (Lemma 6.3.2 and Exercise 6.10).