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

def DoldKan.«termK[_]» : Lean.ParserDescr

def DoldKan.«termN[_]» : Lean.ParserDescr