Homology with local coefficients as a functor from pointed, path-connected spaces and $\pi_1$-modules.

Question

A local system of coefficients on a space $X$ is a functor $F\colon \Pi(X)\rightarrow Ab$ from the fundamental groupoid to the category of abelian groups. From this, one can define the homology groups of $X$ with local coefficients $H_*(X,F)$ as done e.g. in chapter VI of Whitehead's book "Elements of homotopy theory". Therein, it is also shown that this construction yields functors $H_i$ from the category of spaces with local coefficients (a morphism between (X,F) and (Y,G) is a continuous map $f\colon X\rightarrow Y$ with a natural transformation $\eta\colon F\rightarrow f^*G$) to the category of abelian groups.

Suppose now that $X$ is path-connected and has a base point $x\in X$. Then the inclusion $\pi_1(X,x)\rightarrow \Pi(X)$ is an equivalence of categories, so we can pick an inverse functor $i\colon \Pi(X)\rightarrow \pi_1(X,x)$. If we have an module $F$ over $\pi_1(X,x)$ (which is the same as a functor $\pi_1(X,x)\rightarrow Ab$), we get a functor $\Pi(X)\rightarrow Ab$ by $F\circ i$.

Hence, we can define the homology groups of $X$ with local coefficients in the $\pi_1(X,x)$-module $F$ as $H_*(X,F):=H_*(X,F\circ i)$.

First question: Why is this definition independent of the chosen inverse $i$?

It seems to be a common thing to identify local coefficient systems over a path-connected space with modules over the fundamental group at a chosen point, so this has to be true.

Second question: Does this definition extend to a functor $H_i$ from the category of pointed path-connected spaces $(X,x)$ with modules over $\pi_1(X,x)$, where morphisms between $(X,x,F)$ and $(Y,y,G)$ are continuous maps $f\colon X\rightarrow Y$ together with an $\pi_1(f)$-equivariant map $F\rightarrow G$.

As the identification mentioned above is abundant in books and papers within algebraic topology, this should be true as well, but I encounter difficulties in proving this. The main problem seems to be that it might not be possible to choose the inverses $i\colon\Pi(X)\rightarrow \pi_1(X,x)$, such that they form a natural transformation.

Answer 1

1. Inverses are unique up to unique isomorphism: that is, if $F : C \to D$ is a functor and $G_1, G_2 : D \to C$ are two inverses to it, there's a unique natural isomorphism $G_1 \cong G_2$ compatible with the data of being an inverse. (This might require some subtle modifications to the naive notion of "the data of being an inverse": a definition that should be fine is a left adjoint where the unit and counit are isomorphisms.)

2. Yes, everything is fine. Maybe I misunderstand your question, but I don't even see why you need to pick inverses for this statement: there are natural maps $\pi_1(X, x) \to \Pi_1(X)$ of groupoids and you just need to pull back local systems along these maps.