The real projective spaces in homotopy type theory

Ulrik Buchholtz, Egbert Rijke

Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reaso…