202507131607

Tags : Homotopy Type Theory

Interval implies Function Extensionality

---

Lemma

Let $f,g:A\to B$ are two function such that $f(x)=g(x)$ for every $x$ then $f=g$ in the type $A\to B$.

We need to build an element of type ${\prod }_{x:A}f(x)=g(x)$. So for all $x:A$ we define a function. For all $x:A$ we define ${\tilde{p}}_x:I\to B$ give by

$$\begin{array}{rl}{\tilde{p}}_x(0_I)& :\equiv f(x)\\ {\tilde{p}}_x(1_I)& :\equiv g(x)\\ {\tilde{p}}_x(\text{seg})& :\equiv p(x)\end{array}$$

We now define $q:I\to (A\to B)$ by

$$q(i):\equiv \lambda x.{\tilde{p}}_x(i)$$

Then we have $q(0_I)$ is the function $f$ and $q(1_I)$ is the function $g$ so we get $q(\text{seg}):f{=}_{(A\to B)}g$.

Proof coming soon

---

References

• Function Extensionality
• Interval