mathlib

c920a07a - pseudofunctor transfer by adjunction