Cellular cohomology in homotopy type theory

MaRDI QIDQ5114825zbMATH OpenFDO

Authors Ulrik Buchholtz, Kuen-Bang Hou (Favonia)

Publication date 26 June 2020

Full work available at URL https://arxiv.org/abs/1802.02191, https://lmcs.episciences.org/6518

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Cellular Cohomology in Homotopy Type Theory
• Synthetic integral cohomology in Cubical Agda
• Eilenberg-MacLane spaces in homotopy type theory
• The Hurewicz theorem in homotopy type theory
• Homotopy limits in type theory

Cites work

• scientific article; zbMATH DE number 4122835 (Why is no real title available?)
• scientific article; zbMATH DE number 2103273 (Why is no real title available?)
• scientific article; zbMATH DE number 937418 (Why is no real title available?)
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory
• Axiomatic Approach to Homology Theory
• Computational higher-dimensional type theory
• Cubical type theory: a constructive interpretation of the univalence axiom
• Homotopy type theory in Lean
• Meaning explanations at higher dimension
• On higher inductive types in cubical type theory
• The Cayley-Dickson construction in homotopy type theory
• The independence of Markov's principle in type theory
• \(\pi _{n }(S ^{n })\) in homotopy type theory

Cited in

(5)

• Cellular Cohomology in Homotopy Type Theory
• Synthetic integral cohomology in Cubical Agda
• Attaching cells and the rational homotopy type
• Cellularization of structures in stable homotopy categories
• The Hurewicz theorem in homotopy type theory

Describes a project that uses

Uses Software

• GitHub
• cubicaltt

This page was built for publication: Cellular cohomology in homotopy type theory

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