Decades ago, Voevodsky constructed the six-functor formalism in motivic homotopy theory [Ayoub's thesis]. This construction seems very technical, long and "hard".

Very recently [Mann's thesis], the six-functor formalism has been defined to be a lax symmetric monoidal functor $D:Corr(C,E)\rightarrow Cat_\infty$ such that the induced functors $\otimes,f^*$ and $f_!$ have right adjoints. This construction is concise and short.

Question: Are the two constructions "equivalent"? Would Mann's definition surprise Voevodsky or would he just say: "this is exactly what I meant."?

Decades ago, Voevodsky constructed the six-functor formalism in motivic homotopy theory [Ayoub's thesis]. This construction seems very technical, long and "hard".

Very recently [Mann's thesis], the six-functor formalism has been defined to be a lax symmetric monoidal functor $D:Corr(C,E)\rightarrow Cat_\infty$ such that the induced functors $\otimes,f^*$ and $f_!$ have right adjoints. This construction is concise and short.

Question: Are the two constructions "equivalent"? Would Mann's definition surprise Voevodsky or would he just say: "this is exactly what I meant."?