Path spaces of higher inductive types in homotopy type theory

DOI10.5555/3470152.3470159MaRDI QIDQ6654472FDOQ6654472

Authors: Nicolai Kraus, Jakob von Raumer 

Publication date: 19 December 2024

Recommendations

• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• The Seifert-van Kampen Theorem in Homotopy Type Theory
• Homotopy type theory in Lean
• The equivalence of the torus and the product of two circles in homotopy type theory
• Inductive types in homotopy type theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

This page was built for publication: Path spaces of higher inductive types in homotopy type theory

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