« Species of Types
Function Extensionality
[008T]
TODO, follows from univalence.