The real projective spaces in homotopy type theory

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.