Cohomology with dependent coefficients

[felixwellen]

At least the definition of cohomology of a type X can be generalized to dependent coefficients. This means the coefficients are given as a dependent type F : X -> Sp with values in the type of spectra. The usual definition of cohomology with coefficients in an abelian group A can be recovered by setting F to the constant function with value the Eilenberg-MacLane Spectrum of A. Cohomology with non-constant coeffcients can be used to reason about sheaf cohomology internally in a topos. Also, in plain HoTT, it is needed to construct the Serre-Spectral-Sequence. There are a couple of PRs aimed at implementing cohomology in this generality:

• Basic definitions: #723 .
• Pi of dependent spectra: #731
• Covariance in coefficients: #726

[kangrongji]

I know that using ℤ as indexes has advantages as it's easier to define negative-degreed cohomology. But some important construction (e.g. spectrification) needs indexed HIT, and it makes pattern matching impossible since maps like suc are not constructors. Should we use ℕ index instead?

[felixwellen]

Hm, I see. I never thought of the spectrification as indexed, because I only thought about spectrifying suspension spectra... So far, there is nothing specific to the Integer - I think the only thing I use is the successor structure. I took the hint from Floris' thesis to use an abstract successor structure. Maybe that it something we should use as far as possible and really only fix when we have - e.g. in the case of spectrification we can fix it to (Nat,suc). I'm not sure what to do, so I would just go on, as long as I don't do anything specific to the intergers.