Rename ext -> funext.
Rename cong -> ap.
Simplify extensionality for M types.
Rename ⊚ -> ·.