feat(library/hott) add theorem: assuming function extensionality, precomposing and postcomposing of equivalences is an equivalence