Right adjoint of internal category functor?