# Homotopy Type Theory cohomology (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

## Idea

Cohomology groups? are algebraic invariants of types?. Often, they are much easier to compute than homotopy groups . There are many theorems in classical algebraic topology relating them other invariants such as the universal coefficient /theorem and the Hurewicz theorem theorem. (which as of 17/10/2018 have not been proven yet).

Ordinary cohomology denotes cohomology groups with coefficients in $\mathbb{Z}$ this is usually difficult to compute for most spaces, so they are usually broken up into groups for each prime $p$ with coefficients in $\mathbb{Z}_p$. These can be glued back together via the universal coefficient theorem.

## Definition

There are many different flavours of cohomology, but it’s usually best to start simple and add features according to its use.

Let $K(G,n)$ be the Eilenberg-MacLane space of an abelian group? $G$ for some $n : \mathbb{N}$. The (reduced) ordinary cohomology group (of degree $n$ with coefficients in $G$) of a pointed space $X$ is the following set:

$\bar{H}^n(X ; G) \equiv \| X \to^* K(G,n) \|_0$

Note that there is a H-space structure on $K(G,n)$ naturally, so for any $|f|,|g| : H^n(X;G)$ we can construct an element $|\lambda x . \mu(f(x),g(x))| : H^n(X; G)$, hence we have a group?.

Note for any type $X$ we can make this the unreduced cohomology (and call it $H$ instead of $\bar{H}$) by simply adding a disjoint basepoint to $X$ giving us $X_+ \equiv X + 1$ making it pointed.

Let $E$ be a spectrum, we can define the (reduced) generalized cohomology group of degree $n$ of a pointed space $X$ is defined as:

$\bar{H}^n (X; E) \equiv \| X \to E_n \|_0$

note that $E_n$ has a natural H-space structure as by definition we have $E_n \simeq \Omega E_{n+1}$ giving us the same group operation as before. In fact, ordinary cohomology becomes a special case of generalized cohomology just by taking coefficients in the Eilenberg-MacLane spectrum? $HG$ with $(HG)_n \equiv K(G,n)$.