Towards Constructive Homological Algebra in Type Theory

Thierry Coquand (1) , Arnaud Spiwack (2, 3)

1 Division of Computing Science
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 TYPICAL - Types, Logic and computing

This paper reports on ongoing work on the project of representing the Kenzo system in type theory.

Domaines: Logique en informatique [cs.LO]; Catégories et ensembles [math.CT]; Topologie algébrique [math.AT]

Thierry Coquand, Arnaud Spiwack. Towards Constructive Homological Algebra in Type Theory. CALCULEMUS 2007, Jun 2007, Hagenberg, Austria. 12 p., ⟨10.1007/978-3-540-73086-6_4⟩. ⟨inria-00432525⟩