There are a family of fibrations called "generalised hopf fibrations". 

For the real hopf fibrations we have:
S⁰→Sⁿ→ℝℙⁿ
For the complex (usual) hopf fibrations we have:
S¹→S²ⁿ⁺¹→ℂℙⁿ
For the quarternionic hopf fibrations we have:
S³→S⁴ⁿ⁺³→ℍℙⁿ
And finally (only when n <= 2) we have the octionic hopf fibrations:
S⁷→S⁸ⁿ⁺⁷→𝕆ℙⁿ

This screams to me an alternative definition for ℝℙⁿ (and maybe ℂℙⁿ,...)

Inductive RP (n:ℕ) :=
  | map : Sⁿ -> RP n
  | glue : (x y:S⁰) -> map(in x) = map(in y)

Where in : S⁰→Sⁿ is the obvious inclusion map.

Now showing that this is equivalent to the usual definition would 
essentially require a construction of the fibrations they were defined 
from. This fibration is not so easy however, as we cannot 'cheat' and use 
the H-space fibration.

Now the main advantage I see with this definition is that it allows the 
complex, quarterionic etc. projective spaces to be constructed similarly. I 
don't think anybody has constructed quarternionic projective space although 
it should definitely be doable. the main questions arise when octionic 
projective space is considered as in classical AT it degernates pretty 
quickly. (Does this still happen in HoTT, if yes, how so?).

Finally a disclaimer, I thought about these whilst traveling and haven't 
had the time to really put some meat on them. Though hopefully it might 
strike a chord with anyone who has considered a similar thing.

I would love to hear your thoughts and feelings about such things.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.