# Notations for the Dold-Kan equivalence #

This file defines the notation `K[X] : ChainComplex C ℕ`

for the alternating face
map complex of `(X : SimplicialObject C)`

where `C`

is a preadditive category, as well
as `N[X]`

for the normalized subcomplex in the case `C`

is an abelian category.

(See `Equivalence.lean`

for the general strategy of proof of the Dold-Kan equivalence.)

The alternating face map complex, on objects

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The normalized Moore complex functor, on objects.

## Equations

- One or more equations did not get rendered due to their size.