Hom(A, \emptyset) non-empty?

Stream: new members

[Vasily Ilin]

Hi. I am going through the Natural number game https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/. One of the levels is to construct an element of (P -> Q) -> ((Q -> empty) -> (P -> empty)). As a mathematician, I think of the set P -> empty as being empty. Therefore, the set (P -> Q) -> ((Q -> empty) -> (P -> empty)) should be empty. And yet we seem to successfully construct an element of it. What is going on here?

[Bolton Bailey]

P -> empty is usually empty. But what if P is itself empty? Is P -> empty empty then?

[Vasily Ilin]

Well, a function from A to B is a subset of the Cartesian product AxB, so if both are empty, yes, Hom(A,B) is empty.

[Bolton Bailey]

So the cartesian product AxB is empty, but the set of subsets of the cartesian product is not empty. The empty set is an element of that set.

[Vasily Ilin]

if both are empty, yes, Hom(A,B) is empty.

I suppose this does not mesh well with the category theoretic approach, since Hom(A,A) must include the identity for any A.

[Vasily Ilin]

Bolton Bailey said:

So the cartesian product AxB is empty, but the set of subsets of the cartesian product is not empty. The empty set is an element of that set.

Sure, the powerset of AxB is non-empty. I don't see how it solves the problem. We want to construct an element of A -> empty, where A is P -> Q, and is non-empty (in general).

[Adam Topaz]

Hint: there is a unique function from the empty set to any other set (even to the empty set). Try to formalize this in lean!

[Bolton Bailey]

Perhaps another helpful way to think about this is to replace empty with another arbitrary set R. If you were asked to make a function (P -> Q) -> ((Q -> R) -> (P -> R)) for any R, could that be done category-theoretically?

[Bolton Bailey]

To specifically answer your question, you are not trying construct an element of A -> empty, which might be empty even if you have P -> Q. You are trying to construct an element of (Q -> empty) -> (P -> empty), which is never empty if you have an element of P->Q.

[Vasily Ilin]

Okay, I understand! The set (Q -> empty) -> (P -> empty) contains exactly one element. So we have a (unique) function from (P -> Q) to the set with one element.