Cleaned up Univalence -> Funext somewhat