alt Hacker NewsHelp me out, I feel dumb.
The first criterion for a function is stated as:
> The first item in each pair comes from A.
The counter-evidence for the proposition says:
> Let A = {}, and B = {1}. Let f: A -> B = {}
How does this f satisfy the first criterion, if A is uninhabited? It feels like this function can't be invoked. Am I thinking too much in terms of types here?
When there are no pairs, its certainly true that the first element of each pair comes from A. Just like if there are no living dinosaurs its true that all living dinosaurs speak English.