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