Function of empty codomain

Stream: maths

[Matt Yan]

Can somebody help me understand function wolrd, level 8 of the natural numbers game? I know relevant set theory but I'm clueless in HoTT. If you define functions as relations (sets of ordered pairs), for h to be a function, Q has to be the empty set too, see mathoverflow. Apply the same argument to f: P -> Q, we see P also is necessarily an empty set. Thus the construction is impossible - you can't construct an instance of (P -> Q) -> ((P -> empty) -> (Q -> empty) ) for arbitrary sets, P and Q both have to be the empty set

[Yaël Dillies]

You wrote the exercise wrong. It's (P → Q) → ((Q → empty) → (P → empty))

[Matt Yan]

thanks for the correction

[Yaël Dillies]

So you're asked to prove something hard, namely that P is the empty set. But also you have hard (aka strong hypotheses), so maybe you can prove it after all?

[Matt Yan]

I don't understand, am I asked to construct an instance of a certain type for arbitrary P and Q? the type being (P → Q) → ((Q → empty) → (P → empty))

[Kevin Buzzard]

I'm also clueless in HoTT but I wrote the natural number game. Your claims are false. If P is nonempty then P -> empty exists, it's just empty. I claim that you can construct the instance for all P and Q.

[Kevin Buzzard]

Mathematicians write Hom(X,Y) for the type that Lean refers to as X -> Y, if this helps (this notation confused me for a while when I was learning this stuff)

[Kevin Buzzard]

For example, if P and Q are nonempty then I'm asking you to write down a function which takes a map from P to Q and returns a map from the empty set to the empty set, and this can certainly be done.