The real projective spaces in homotopy type theory

Thursday, April 5, 2018 - 12:00

427 Thackeray Hall

Speaker Information
Egbert Rijke
Carnegie Mellon University

Abstract or Additional Information

We will show how the real projective spaces are defined in homotopy type theory, together with the tautological  S^0-bundle over it. Furthermore we define the orthogonal complement of the tautological bundle is defined, and show that it trivializes when we take the Whitney sum with the tautological bundle.