[[!redirects The real projective spaces in homotopy type theory]] < [[nlab:The real projective spaces in homotopy type theory]] category: redirected to nlab