Does the curried version of a bifunctor contain more information?

139 Views Asked by At

For functions $f:X\times Y\to Z$, the curried version $\lambda f:X\to (Y\to Z)$ is a different way of representing the exact same information.

For functors, I’m assuming that the same should hold, but intuitively I’m thinking that the curried version contains more information.

Consider the similar case for a bifunctor. Given categories $C,D,E$, consider the functor $F:C\times D\to E$. We can curry this using the exponential category, and get the functor $\lambda F : C \to E^D$.

With the base functor $F$, we can EITHER input an object $(c,d)$ OR a morphism $(f,g)$ where $c,d$ are objects and $f,g$ morphisms of $C$ and $D$ respectively. In these two cases we get objects and morphisms in $E$ out of them.

But with the curried functor, we have more options: We can first input an object $c$, and then input an object $d$, which gives us the same as inputting $(c,d)$. We can also input first $c$ and then a morphism $g\in D$. Alternatively, we can immediately input a morphism $f\in C$ into $\lambda F$.

Doesn’t this increased amount of uses of $\lambda F$ mean that it has more information than $F$?

1

There are 1 best solutions below

4
On BEST ANSWER

Immediate intuitive answer: it can't, because things ought to be well-behaved, which means that currying ought to be an equivalence of the appropriate categories (in this case: $\mathsf{Fun}(C \times D, E)$ and $\mathsf{Fun}(C, E^D)$) which means it ought to be reversible.

Let's chase down what happens in the curried version of the functor $\lambda F$. If we put in an object $c \in C$, this will get sent to what is informally referred to as $F(c, -)$. This functor takes an object $d \in D$, and sends it to $F(c, d)$. So what does it do on morphisms? Given $g: d \to d'$, we need to get a morphism $F(c, g): F(c, d) \to F(c, d')$, and the only reasonable definition is to have $F((\mathrm{id}_C, g))$, and you can check that this works. Thus: the information of what happens when you first put an object, and then a morphism, into $\lambda F$ is already contained in $F$: you just use the identity morphism of the object.

For the other direction: if $f: c \to c'$ is a morphism, $\lambda F(f) = F(f, -)$ ought to be a morphism from $F(c, -) \to F(c', -)$. That is, for each $d \in D$ we should have a morphism $F(c, d) \to F(c', d)$. Again our only real choice is to have this be $F((f, \mathrm{id}_D))$. Again, you can check that this works.