How to understand the cardinality of Yoneda in the case of unit?

Question

Note that this isn't strictly a haskell question, but that's where I've been playing around with this and where I've seen the yoneda lemma expressed most cleanly...

So, with the yoneda lemma, we know that

forall x . (a -> x) -> f x ~= f a

But what I'm wondering is, how does this work for the type x when it is of lower cardinality than a? For example, unit...taking f=Identity, a=Integer, x=Unit we get something like

(Integer -> ()) -> Indentity () ~= Identity Int

Which seems to make no sense?

I've always thought of yoneda in the terms of, say, a=Bool and x=Int

(Bool -> Integer) -> Identity Integer ~= Identity Bool

Where in a sense, Identity Integer "seems" larger than Identity Bool, but given the fact that it had to have been built by a Bool->Integer, we know that there are in fact only two options...but I feel like flipping it shows that said understanding is not quite right.

I'd appreciate any help understanding this!

Answer 1

You can't fix x ~ (). For the identity to hold, the function must work for every choice of x, not just a single specific choice. That's why there's a forall on that parameter. So let's recast your example, remaining parametric over x. I give you a function of the following type

(Integer -> x) -> Identity x

promising that it works for any x that you choose. The only way I could possibly implement this function is to have an Integer in my hand already, and call the function you give me on it, yielding an x. Thus, my function is equivalent to an Identity Integer.

Likewise we can take a ~ Bool, f ~ [], yielding

(Bool -> x) -> [x]

The only way I can implement this is if I have a [Bool] lying around, and call your function with each of my Bools.

Since x must be polymorphic, it has no particular cardinality, and so the question of being smaller or larger than a does not arise.