I was just reading Mike Shulman's [blog post](https://homotopytypetheory.org/2013/07/24/cohomology/) on how to define cohomology in homotopy type theory (HoTT), and I was curious if we can similarly define cohomology with local coefficients in HoTT as well?


I know that a local system can be viewed as a locally constant sheaf, as a covering space (the corresponding étalé space of the sheaf), or as a representation of the fundamental groupoid. I am most familiar with the sheaf definition of cohomology with local coefficients, but I assume that one of the latter two points of view will be the right way to approach it here?


My naïve guess would be that if $C$ is the covering space corresponding to a representation of the fundamental groupoid of $X$, then we would just use the same definition as in the blog post, with $$H^n(X;C) := \| X \to \Omega^{-n} C \|\_0.$$
But I'm not sure how we can choose the deloopings of $C$ in this case.


I'm still learning HoTT, so I apologize if this is obvious.



Cohomology with local coefficients in homotopy type theory
*(I suppose this is actually an answer, so I should post it as one.)*


Yes, this generalization is described in the [next blog post](https://homotopytypetheory.org/2013/08/08/spectral-sequences/), since it's needed for the Serre spectral sequence. Make sure you read the version [here](https://ncatlab.org/homotopytypetheory/show/spectral+sequence#spectral_sequences_in_hott_2) with the math. The local coefficients appear towards the bottom, starting with the paragraph "First we have to generalize our notion of cohomology a bit."


