Closed functors - Category theory

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

Asad Saeeduddin

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

Asad Saeeduddin

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

Asad Saeeduddin

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