I'm reading Michael Shulman's articles on cohomology in HoTT [here](https://homotopytypetheory.org/2013/07/24/cohomology/) and [here](https://ncatlab.org/nlab/show/spectral+sequences+in+homotopy+type+theory), as well as Floris van Doorn's thesis [here](https://florisvandoorn.com/papers/dissertation.pdf).


Given $E: Z \to \mathsf{Spectrum}$ a family of spectra over a homotopy type $Z$, they define the parametrized (or twisted) cohomology of $Z$ with coefficients in $E$ by
$$H^n(Z; E) :\equiv \pi\_0\left( \prod\_{x \in X} E\_n(x) \right)$$
where $\prod\_{x \in X} E\_n(x)$ denotes the appropriate type of sections. In the special case that we have a family of abelian groups $A: X \to \mathsf{AbGroup}$ then the composite with the Eilenberg-Mac Lane construction $H: \mathsf{AbGroup} \to \mathsf{Spectra}$ gives us a parametrized family of Eilenberg-Mac Lane spectra $HA: X \to \mathsf{Spectra}$. The corresponding twisted cohomology is cohomology with local coefficients.


Though they don't discuss it in their articles, I am wondering if we can get long exact sequences in parametrized cohomology starting from a cofibre sequence of types? I can see how you do it for unparametrized spectra, but the pi-types in parametrized cohomology make it a bit more confusing.


Specifically, suppose that I have a homotopy cofibre sequence $X \xrightarrow{f} Y \xrightarrow{q} C\_f$ equipped with a parametrized spectrum $E: C\_f \to \mathsf{Spectrum}$.
Clearly I can pull back along $q$ and $q \circ f$ to get parametrized spectra $q^\*E:=E \circ q: Y \to \mathsf{Spectrum}$ and $f^\*q^\*E:=E \circ q \circ f: X \to \mathsf{Spectrum}$. Does the above cofibre sequence give me a long exact sequence in parametrized cohomology?



Long exact sequences for parametrized cohomology
$\require{AMScd}$Yes. It is better to consider the more general situation of a pushout square of types, since pushout squares (unlike cofiber sequences) are stable under base change. Then the difference between parametrized and unparametrized disappears, since one can work in the $\infty$-topos over the pushout.


More generally, consider a pushout square
\begin{CD}
A @>>> B\\
@VVV @VVV\\
C @>>> D
\end{CD}
in an $\infty$-topos $T$ and a family of spectra $E$ over $D$. Then the induced square of global sections (where the pullbacks of $E$ are implicit)
\begin{CD}
\Gamma(D,E) @>>> \Gamma(C,E)\\
@VVV @VVV\\
\Gamma(B,E) @>>> \Gamma(A,E)
\end{CD}
is cartesian, hence gives rise to a long exact sequence of parametrized cohomology groups
$$
\dots\to \pi\_{n+1}\Gamma(A,E) \to \pi\_n\Gamma(D,E) \to \pi\_n\Gamma(B,E)\times \pi\_n\Gamma(C,E)\to\dots.
$$


The statement for a family of spectra $E$ is equivalent to the statement for each family of types $\Omega^{\infty-i}E$ (which gives the above long exact sequence up to the product of $\pi\_{-i}$'s), so it suffices to consider a family of types. By the descent property of $\infty$-topoi, we have cartesian square of $\infty$-categories
\begin{CD}
T\_{/D} @>>> T\_{/C}\\
@VVV @VVV\\
T\_{/B} @>>> T\_{/A}
\end{CD}
The cartesian square of global sections is then a special case of the assertion that mapping spaces in a limit of $\infty$-categories are the limits of the mapping spaces.
Alternatively, we can pass to spectrum objects to obtain a cartesian square of stable $\infty$-categories, and there is an analogous assertion about mapping spectra in a limit of stable $\infty$-categories.


