Proof of the Dold-Kan equivalence in Lean

Get the code using leanproject get joelriou/dold-kan.

The general strategy of the proof is explained in equivalence.lean.

Dependency graph

PDF version of the graph