Corollary 3.6.
Assuming that:
the diagram
is a commutative square of
categories
and
functors
all the
functors
have
left adjoints
Then
the square of
left adjoints
commutes up to natural isomorphism.