As Dan said, this is not a correct definition of RP^n.
More specifically, the issue is that you identified the points "map south" and "map north" in two different ways: "glue south north" and "inv (glue north south)".
You could try to add another constructor
glue² : (x y : S^n) -> glue x y = inv (glue y x)
but of course you're now again identifying them in two different ways, so you've just shifted the problem one dimension up.
Den lör 18 aug. 2018 16:46Dan Christensen <
jdc@uwo.ca> skrev:
On Aug 18, 2018, Ali Caglayan <alizter@gmail.com> wrote:
> 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.
That HIT would be S^n with four edges attached: two edges connecting
the north pole to the south pole, and a self-loop at each pole. So
homotopically it would be S^n wedged with a wedge of four circles.
To get the right space with the right bundle over it, see:
The real projective spaces in homotopy type theory
Ulrik Buchholtz, Egbert Rijke
https://arxiv.org/abs/1704.05770
Dan
--
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.