Joaquín Rodriguez comments on Extensionality and the univalence axiom of type theory