Using HoTT, why is twisted cohomology of BG group cohomology?

Question

I've been reading Michael Shulman's blog posts defining cohomology in homotopy type theory, and I'd like to understand (using HoTT) why cohomology of BG is group cohomology.

if I understand correctly, given a parametrized spectrum (i.e. a fibration by spectra) $E: X \to \mathsf{Spectra}$, we define the twisted cohomology of $X$ with coefficients in $E$ to be $H^n(X; E) \equiv \Vert \prod_{x:X} \Omega^{-n} E_0 \Vert_0$.

In particular, if we have a parametrized family $V: X \to \mathsf{AbGroup}$ then we can compose with the Eilenberg-MacLane construction $H: \mathsf{AbGroup} \to \mathsf{Spectra}$ to get a parametrized family of Spectra $HV: X \to \mathsf{Spectra}$. The cohomology $H^n(X; HV)$ is cohomology with local coefficients, which is the twisted version of ordinary cohomology.

Now if we consider the case $X = BG$ (i.e. $BG=K(G,1)$ ) for $G$ a set-group, then a parametrized family $V: BG \to \mathsf{AbGroup}$ is the same as a group representation of $G$, since functions are functorial on paths in HoTT. In other words, given $g: \bullet = \bullet$, we get a path $g_*: V(\bullet) = V(\bullet)$. Now, if we consider the corresponding twisted cohomology $H^n(BG; HV) \equiv \Vert \prod_{x:BG} K(V(x);n) \Vert_0$, why do we get group cohomology?

For now let's just consider $H^0(BG; HV) \equiv \Vert \prod_{x:BG} V(x) \Vert_0 = \prod_{x:BG} V(x)$, where the second equality follows because $V(x)$ is a set. In order to get group cohomology, it should be the case that any $v: \prod_{x:BG} V(x)$ encodes a $G$-invariant element of the $G$-representation. But it isn't immediately obvious to me why this should be the case.

Any help would be greatly appreciated!

Answer 1

There's not really much to say (which is why I'm marking this answer as CW):

As Phil Tosteson commented, forming $\Pi$-types is right adjoint to the constant family map $\mathcal{U} \to \mathcal{U}^{BG}$ (and $\Sigma$-types gives the left adjoint). So that's the universal property of invariants (and co-invariants).

Perhaps it would help to see what happens if $G$ is a $1$-group: We can present $BG$ as a HIT with constructors $$ \text{pt} : BG, \quad \text{loop} : G \to \text{pt}=\text{pt},\quad \text{loop-cmp} : \prod_{g,h:G}\text{loop}(g\cdot h) = \text{loop}(g)\cdot\text{loop}(h), $$ as well as a constructor forcing $BG$ to be a $1$-type. If $V : BG \to \text{Set}$ is any $G$-set, then by the universal property of $BG$ as a HIT, we get an equivalence $$ \prod_{t:BG}V(t) \simeq \sum_{v:V(\text{pt})}\prod_{g:G}g\cdot v = v.$$ (Since $V$ is a family of sets, there's nothing to do for the $\text{loop-cmp}$ constructor.)