The real projective spaces in homotopy type theory

zbMath1452.03033arXiv1704.05770MaRDI QIDQ5144693

Egbert Rijke, Ulrik Buchholtz

Publication date: 19 January 2021

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

zbMATH Keywords

homotopy type theoryunivalence axiomreal projective spaceshigher inductive types

Mathematics Subject Classification ID

Eilenberg-Mac Lane spaces (55P20) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Related Items (7)

Modalities in homotopy type theory ⋮ From reversible programs to univalent universes and back ⋮ The construction of set-truncated higher inductive types ⋮ Duality notions in real projective plane ⋮ Unnamed Item ⋮ Higher Structures in Homotopy Type Theory ⋮ On Small Types in Univalent Foundations

This page was built for publication: The real projective spaces in homotopy type theory