I just read Mike Shulman's blog post the other night, discussing the definition of cohomology in Homotopy Type Theory. I really enjoyed the new (to me) perspective, but I had a few questions on technicalities.
Given types $X$ and $Y$, Mike defines
$$H^n(X; Y) :\equiv \| X \to \Omega^{-n} Y \|_0.$$
This agrees with the definition given in the nLab article on cohomology. Here is where my first question comes up:
- Although it's not stated in the article, I assume that for $n \neq 0$ we need $Y$ to be a pointed type, since (if I understand correctly) looping/delooping requires a choice of basepoint? Or does it not matter?
(Mike does explain in the article that for $n>0$ we need to specify choices of deloopings, since deloopings might not exist and might not be unique, and that we usually just take $Y$ to be a spectrum so that this works.)
However, in section 1.1 of this paper on Eilenberg-MacLane spaces in HoTT by Daniel Licata and Eric Finster they seem to be saying that the definition above actually produces reduced cohomology, since they write:
On the other hand, in his blog post Mike writes defines reduced cohomology for pointed types $X$ and $Y$ by
$$\tilde{H}^n(X; Y) :\equiv \| \operatorname{Map}_*(X, \Omega^{-n} Y) \|_0.$$
(He technically defines it only in the case that $Y$ is a spectrum, but I'm extrapolating here.) So this leads me to my second question:
- What is the correct definition for reduced cohomology in HoTT?
Best Answer
In order for the notation $\Omega^{-n} Y$ to make sense for $n \ge 1$, $Y$ must be a grouplike $E_n$-space, which in particular means it has a basepoint (the identity of the $E_n$ multiplication). For $n \le -1$ we also need a basepoint to define the based loop space. However note that $X$ does not need to have a basepoint.
As far as I can tell, the excerpt from Licata-Finster is incorrect; it gives ordinary cohomology, not reduced cohomology. Mike Shulman's definition is the correct one.