Towards Constructive Homological Algebra in Type Theory

DOI10.1007/978-3-540-73086-6_4MaRDI QIDQ5428258zbMATH OpenOpenAlexFDO

Authors Thierry Coquand, Arnaud Spiwack

Publication date 28 November 2007

Published in Towards Mechanized Mathematical Assistants (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/inria-00432525/file/v2.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Other constructive mathematics (03F65) Software, source code, etc. for problems pertaining to category theory (18-04) Homological algebra in category theory, derived categories and functors (18G99) Symbolic computation and algebraic computation (68W30)

Recommendations

• Homotopy-initial algebras in type theory
• Homotopy type-theoretic interpretations of constructive set theories
• The homotopy theory of type theories
• Exploring abstract algebra in constructive type theory
• Homotopy type theory
• Homotopy Type Theory
• Homotopy Type Theory: A synthetic approach to higher equalities
• Higher Structures in Homotopy Type Theory
• Type theory and homotopy
• Homotopy type theory and the formalization of mathematics

Cited in

(20)

• \(MP\)-algebras with relative types
• Kenzo
• Formalization of a normalization theorem in simplicial topology
• Higher inductive types as homotopy-initial algebras
• Mini-workshop: Constructive homological algebra with applications to coherent sheaves and control theory. Abstracts from the mini-workshop held May 12--18, 2013.
• Pro-algebraic homotopy types
• Proof Pearl: Revisiting the Mini-rubik in Coq
• ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
• scientific article; zbMATH DE number 3949678 (Why is no real title available?)
• scientific article; zbMATH DE number 2109817 (Why is no real title available?)
• Coherent and Strongly Discrete Rings in Type Theory
• scientific article; zbMATH DE number 1420784 (Why is no real title available?)
• Homotopy Type Theory: A synthetic approach to higher equalities
• scientific article; zbMATH DE number 7561488 (Why is no real title available?)
• Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
• Univalent categories of modules
• Effective homology of bicomplexes, formalized in Coq
• Topological quantum gates in homotopy type theory
• A mechanized proof of the basic perturbation lemma
• Generating certified code from formal proofs: a case study in homological algebra

This page was built for publication: Towards Constructive Homological Algebra in Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5428258)