Corollary 3.6. Assuming that:

Then the square of left adjoints commutes up to natural isomorphism.