wrong reference to a no loger existing appendix about univalence implies extensionality changed to a reference to an existing section