Formalizing equivalences without tears

DOI10.4230/LIPICS.TYPES.2024.1MaRDI QIDQ7292883zbMATH OpenFDO

Authors Thomas de Jong

Publication date 8 July 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2024.1

Mathematics Subject Classification ID

Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Cites work

• Extensional constructs in intensional type theory
• Homotopy type theory. Univalent foundations of mathematics
• Homotopy type theory: the logic of space
• Localization in Homotopy Type Theory

This page was built for publication: Formalizing equivalences without tears

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