Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations