In the $\ell$-adic setting a reference would be Laszlo-Olsson's papers on six operations for Artin stacks: http://arxiv.org/abs/math/0512097 http://arxiv.org/abs/math/0603680 http://arxiv.org/abs/math/0606175 Also see: http://arxiv.org/abs/1211.5948 Regarding mixed equivariant derived categories in the Hodge sense, as far as I know there isn't any canonical reference in the literature for this. However, I claim that the Bernstein-Lunts approach (for $X/G$, $G$ linear algebraic) works just fine for mixed Hodge modules (or even $\ell$-adic coefficients, but I am more comfortable with the mixed Hodge setting so not quite as sure about $\ell$-adic). The point is that Bernstein-Lunts mainly just use the six operations in their approach. So everything goes through formally in the same way for mixed Hodge modules. The only place where you might worry is something funny happening with weights. However, there is no problem if all your approximation spaces are algebraic (hence the linear algebraic requirement) and all pushforwards are along proper (algebraic) maps and pullbacks are along smooth (in the algebraic sense) maps. I remember going through things carefully for $B\backslash G/B$ a couple of years ago. Many of these checks are also done in O. Schnurer's thesis. A condensed/article version of the latter can be found here: http://arxiv.org/abs/0809.4785 I would also suggest just asking Wolfgang. I do not know what the state of the art in defining mixed motivic sheaves at the moment is. Some comments not directly related to the question (but I am reading between the lines and assuming this is where you are coming from Jan): As far as graded representation theory type applications go, the desire for a mixed equivariant derived category usually manifests itself in trying to prove splitting of some sequences, purity/formality type results, and/or to get a grading on Ext-spaces. In each of these situations one can avoid having to invoke a high powered theory of mixed equivariant categories by just working on an approximation space and the mixed (non-equivariant) derived category on this space (we are just unwinding the Bernstein-Lunts approach/Borel construction). I would claim that often even working with a mixed (non-equivariant) derived category can be avoided, since usually the only way one has of getting a handle on Ext-spaces is by interpreting them as cohomology of some space, or a convolution algebra formalism, or using a suitable fibre functor (I am thinking along the lines of Soergel bimodules, Geometric Satake, etc.). So as long as you know there is a functorial mixed structure on cohomology groups you can get away without explicitly invoking mixed categories. Having said that, there is one caveat: coming from the graded representation theory perspective, mixed sheaves offer the opportunity to impose gradings in a functorial way (note: Ext-groups in the mixed derived category are ordinary vector spaces, it is Ext-groups in the non-mixed derived category that inherit mixed structures via realization). I don't know how one can (in general) cheat to get these mixed strucures on Ext-spaces that behave functorially. In special situations you can get by via devices like Soergel bimoules, working with $\mathbb{C}^*$-coherent sheaves on cotangent bundles, etc. But these are replacements that require a lot of extra work (often worth it for characteristic $p$ applications). In characteristic $0$ the conceptual approach still would be to go through mixed categories. Of course, getting gradings this way is not at all a triviality: a grading corresponds to having split Tate structures which can be quite difficult to prove (eg. I don't know how see directly that Ext between Vermas, in just the ordinary $G/B$ case is split Tate). In representation theory type settings, there is the (somewhat mysterious) phenomenon that intersection cohomology has a basis given by algebraic cycles (I am thinking Geometric Satake, fibres of the Bott-Samelson resolution etc.). As Wolfgang would (probably) say, if we had a fully functional theory of motivic sheaves all the pain would go away! A comment on Dan Peterson's answer: I am not sure about a 6 functor formalism for simplicial varieties. There is a brief discussion in Bernstein-Lunts about some of the difficulties in defining six functors and proving their properties in this setting (I don't remember the precise section).