Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
The ncatlab article on closed functors defines an extranatural transformation jX:I→[X X]j_X : I \to [X\; X]jX:I→[XX] as part of the data of the category. It also has this commuting diagram:
closed functor law
I don't get how that vertical map squares with the definition of jXj_XjX; isn't it backwards?
The only thing I can imagine is it was meant to be i[X X]i_{[X\; X]}i[XX] instead, since that's an isomorphism
@Christoph explained it in Slack, [− −][-\; -][−−] is contravariant in its first argument
The ncatlab article on closed functors defines an extranatural transformation jX:I→[XX] as part of the data of the category. It also has this commuting diagram:
closed functor law
I don't get how that vertical map squares with the definition of jX; isn't it backwards?
The only thing I can imagine is it was meant to be i[XX] instead, since that's an isomorphism
@Christoph explained it in Slack, [−−] is contravariant in its first argument