Decades ago, Voevodsky constructed the six-functor formalism in motivic homotopy theory [[Ayoub's thesis](https://user.math.uzh.ch/ayoub/PDF-Files/THESE.PDF)]. This construction seems very technical, long and "hard".


Very recently [[Mann's thesis](https://arxiv.org/abs/2206.02022)], 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."?



Voevodsky's six functor formalism VS Lucas Mann's
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.


