202506261706

Tags : Homotopy Type Theory

Homotopy Induction

---

Theorem

Given any $D:{\prod }_{f,g:{\prod }_{a:A}B(a)}(f\sim g)\to \mathcal{U}$ and $d:{\prod }_{f:{\prod }_{a:A}B(a)}D(f,f,\lambda x.{\text{refl}}_{f(x)})$, there exists:

$$k:\prod _{(f,g:{\prod }_{a:A}B(a))}\prod _{(h:f\sim g)}D(f,g,h)$$

such that $k(f,f,\lambda x.{\text{refl}}_{f(x)})=d(f)$ for all $f$.

This is again another way to state Function Extensionality. This is because Function Extensionality simply says that for any type family $B:A\to \mathcal{U}$, the type family

$$(-\sim -):\left(\prod _{a:A}B(a)\right)\to \left(\prod _{a:A}B(a)\right)\to \mathcal{U}$$

together with $\lambda f.\lambda a.{\text{refl}}_{f(a)}$ satisfies the 4th point of Identity System, this is equivalent to version 1.

---

References

• Univalence
• Function Extensionality
• Identity System
• Equivalence Induction