Long exact sequences for parametrized cohomology I'm reading Michael Shulman's articles on cohomology in HoTT here and here, as well as Floris van Doorn's thesis here.
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?
 A: $\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.
