Thursday, April 5, 2018 - 12:00

427 Thackeray Hall

### 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.