Re: [HoTT] Real Projective space (and other projective spaces too)

[Guillaume Brunerie <guillaume.brunerie@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2754 bytes --]

Ah, indeed, I misread the proposed definition.

Den lör 18 aug. 2018 21:35Dan Christensen <jdc@uwo.ca> skrev:

> The extra identifications are one of the problems, but a more
> fundamental problem is that while the north pole has been identified
> with the south pole, no other pairs of antipodal points have been
> identified.
>
> Dan
>
> On Aug 18, 2018, Guillaume Brunerie <guillaume.brunerie@gmail.com> wrote:
>
> > 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.
>
> --
> 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.
>

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

[-- Attachment #2: Type: text/html, Size: 4184 bytes --]