Recently, I began to study $\mathcal{D}$-modules and one of the major problems I encountered is that many natural transformations on the (derived) category of $\mathcal{D}$-modules are defined as the composition of many different morphisms. By this I mean that for any object it is defined a morphism between the image of this object via the two functors, and often it is not checked that this construction is functorial. Moreover, in many proofs these natural transformations are splitted into several natural transformations, but it is not clear to me why this can be done.

Let me give an example so to make things clearer. (Everything I will write can be found in *$\mathcal{D}$-modules, Perverse Sheaves, and Representation Theory*)

Let us consider $X$ a smooth algebraic variety over $\mathbb{C}$ and denote $X^{an}$ the associated complex manifold. Let $f : X \rightarrow Y$ be a morphism of smooth algebraic varieties. We define the direct image of $M^{\cdot} \in D^{b}(\mathcal{D}_X)$ as $$\int_fM^{\cdot} = Rf_{*} \left( \mathcal{D}_{Y \leftarrow X} \otimes^{L}_{\mathcal{D}_X} M^{\cdot}\right) \in D^b(\mathcal{D}_Y)$$ and we define the analytization of a $\mathcal{D}_X$ module as $$(M^{\cdot})^{an} = \mathcal{D}_{X^{an}} \otimes_{i^{-1}\mathcal{D}_X} i^{-1}M^{\cdot}$$ where $i : (X^{an}, \mathcal{O}_{X^{an}}) \rightarrow (X, \mathcal{O}_X)$ is the canonical morphism. There exists a natural morphism $\left( \int_f M^{\cdot} \right)^{an} \rightarrow \int_{f^{an}} (M^{\cdot})^{an}$ which is constructed as the composition of many maps. Hence, it is quite difficult to deal concretly with this morphism and to verify that it is functorial in $M$. Moreover, from the construction of the morphism it is not clear to me why it should hold $$ \left( \int_{f \circ g} M^{\cdot} \right)^{an} \rightarrow \int_{(f \circ g)^{an}} (M^{\cdot})^{an} = \left( \int_{f \circ g} M^{\cdot} \right)^{an} \rightarrow \int_{f^{an}} \left( \int_g M^{\cdot} \right)^{an} \rightarrow \int_{f^{an}} \circ \int_{g^{an}} (M^{\cdot})^{an}. $$ Hence, my question is: the functoriality of some trasformations has to be awlays checked by hand or can it be deduced by a clever way of defining the maps? Moreover, the fact that some trasformations can be splitted into several ones comes from the construction if this is done in a particular way?

Mostly what I would like to understand is that if there is a "correct" (and what does correct mean?) construction of a theory such that it brings easily facts as the ones stated above.