Nilpotent types and fracture squares in homotopy type theory

DOI10.1017/S0960129520000146zbMath1498.18038arXiv1903.03245MaRDI QIDQ5139290

Luis Nerio Scoccola

Publication date: 8 December 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1903.03245

zbMATH Keywords

nilpotent spaceEilenberg-MacLane spacehomotopy type theoryprincipal fibrationfracture square

Mathematics Subject Classification ID

Localization and completion in homotopy theory (55P60) Logic in computer science (03B70) Localization of categories, calculus of fractions (18E35) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Related Items (3)

Localization in Homotopy Type Theory ⋮ The Hurewicz theorem in homotopy type theory ⋮ The Reeb graph edit distance is universal

Cites Work

• Unnamed Item
• Unnamed Item
• The homotopy theory of type theories
• Homotopy limits, completions and localizations
• Eilenberg-MacLane spaces in homotopy type theory
• Higher Groups in Homotopy Type Theory
• Sequential Colimits in Homotopy Type Theory
• Modalities in homotopy type theory
• Localization in Homotopy Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Homotopy limits in type theory

This page was built for publication: Nilpotent types and fracture squares in homotopy type theory