Voevodsky's six functor formalism VS Lucas Mann's 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."?
 A: There may be some confusion in this question about what exactly Voevodsky/Ayoub and Mann do, as they do very different things.

*

*Mann's thesis constructs a formalism of six operations in the setting of rigid-analytic geometry, using some $\infty$-categorical construction techniques developed for this purpose by Liu and Zheng. Along the way he gives an abstract definition of what a "formalism of six operations" is using categories of spans, but this definition was certainly well known and already appears (in a more complete form, see below) in the book of Gaitsgory and Rozenblyum.

*Ayoub's thesis, based on Voevodsky's unpublished ideas, explains how one gets for free a formalism of six operations on the category of schemes out of some very simple axioms (what he calls a "homotopy 2-functor"). These axioms are of a geometric rather than categorical nature. The output of Ayoub's theorem (combined with the $\infty$-categorical construction techniques of Gaitsgory-Rozenblyum or of Liu-Zheng) is in particular a formalism of six operations in the sense of Mann.

Note also that the definition of a formalism of a six operations in Mann's thesis is far from capturing everything. A more complete definition would be a right-lax symmetric monoidal functor from an $(\infty,2)$-category in which both the 1-morphisms and the 2-morphisms are spans (Gaitsgory and Rozenblyum work with an intermediate 2-category, probably for simplicity's sake, in which the 1-morphisms are spans and the 2-morphisms are just morphisms). These 2-morphisms encode the functoriality of bivariant homology, i.e., the isomorphisms $f_!\simeq f_*$ for $f$ proper and $f^!\simeq f^*$ for $f$ étale. But even this does not capture all the structure that we have in the examples, such as the contravariance of bivariant homology with respect to quasi-smooth morphisms.
