Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
At “Definition as a 2-functor”, the article says
For a proarrow and ordinary arrows and , we write for the composite ; it is a proarrow from to . We also write , , or simply for the identity proarrow .
In seems that the nLab has settled on the convention that a profunctor is a functor . Therefore, in the expressions and the morphism is in the covariant slot, which means that either should be a morphism out of or should be a profunctor into .
What am I missing?
It seems right to me. The covariant slot of is the category that it is “from” as a profunctor, and we are substituting a value of into that slot; so it’s correct that is a profunctor from to something else, and that the values of belong to , i.e. that is a morphism into .
In that case, and are the problem. Thinking of as a set of heteromorphisms from to , we can precompose with to get a set of heteromorphisms from to , but to postcompose, we need , not . That is,
is not a morphism in , it’s a functor with codomain , and similarly is not a morphism in , it’s a functor with codomain . We’re not describing the action of the functor on its elements/heteromorphisms; we’re describing its restriction along a pair of functors.
It’s like the multiplication of three matrices (the outer two being special in deriving from functions), if that helps. Or the composition of relations.
Mike: Then shouldn’t it be , that is, followed by followed by the taking the preimage under ? The expression doesn’t make sense; since is the codomain of , having in the other slot means we’d want the domain of . If we want the codomain of , it needs to be in the same slot that is.
The in represents the hom-functor of , which is a profunctor from to . Thus, being a functor with codomain , it can be plugged into either slot of this profunctor.
Although in the context of the quote in question, and are just notations for the two proarrows associated to the arrow . The reason for using that notation is as I said: in the case of categories and profunctors, they are and .
OK, so in that notation, both slots are covariant. I’ll add a note to that effect. Thanks!
I think I have some idea of what you mean, but I don’t think “both slots are covariant” is really the correct way to say it. is still a functor from to , so in that sense the first slot is contravariant. And if the question is what kind of a functor is as a functor of and , then it’s a functor from to , so in that sense also the first slot is contravariant.
1 to 10 of 10