Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

The ncatlab article on closed functors defines an extranatural transformation $j_X : I \to [X\; X]$ 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 $j_X$; isn't it backwards?

The only thing I can imagine is it was meant to be $i_{[X\; X]}$ 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 $j_X : I \to [X\; X]$ 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 $j_X$; isn't it backwards?

The only thing I can imagine is it was meant to be $i_{[X\; X]}$ instead, since that's an isomorphism

@Christoph explained it in Slack, $[-\; -]$ is contravariant in its first argument