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:

  1. 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: enter image description here

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:

  1. What is the correct definition for reduced cohomology in HoTT?
  1. 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.

  2. 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.

  • $\begingroup$ Thank you! Appreciate the clarification. $\endgroup$ – ಠ_ಠ Dec 10 '20 at 0:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.