From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBB7G24DNQKGQEFMSFDWA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-oi0-x23b.google.com (mail-oi0-x23b.google.com [IPv6:2607:f8b0:4003:c06::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6203370a for ; Sat, 18 Aug 2018 14:30:22 +0000 (UTC) Received: by mail-oi0-x23b.google.com with SMTP id 13-v6sf9808835oiq.1 for ; Sat, 18 Aug 2018 07:30:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=TQfwU9R8poU4TDXvBFOiAC9Nqmvq3efGrxjDYGbMUgY=; b=DW/BPs6ZfG/fu71Yxfbn45Uu/leK2Hb/E3mpH2L8ntw6bwoGvlX731l6EMTR6HTona N2hFuFX3PZWOqNXfTlToli3Hawf2z4p7+RUZoBeairsADpcLqki+JZYsEEllZSannSly ztZ1iU7Izp7YIwzHjz9WXcQAi7SMqXo/nxWnYwMFV1E2HkXZ+HgdxXaFLqdK981rizDA +fKmCXIAYf88Vxc1iprMaDjAbjaKvH+rm5bi/AGMPSRI1A6Sk8JqE5bCdJYrCLRjNb3Z Up6XErVQ6I1tEfpxqHYZjwO53wO7vM9GBhH5FwkCkQ/RWn00iyn3Hd3XYHuK3FHyBb9S ke+w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=TQfwU9R8poU4TDXvBFOiAC9Nqmvq3efGrxjDYGbMUgY=; b=F7qJg2Z03AaOJz+hgQdzHGT35k/xTrvO/cEEKANsxgSwB1rZ9M+zgxq7DdyegKPtj9 cMnwrOt9MUZIDUyTaOEb6hFPzRtIVf+ohKBtWpjxnmVs3nFmVTD3xY65I5qs388cUeHV 7FLBzFR2oQBiViEUESoEganti1zEYTq17X84Uhr6C0wRssR9qg74X9WrIcTW2OgWQ4zx TX4+iLp1qrIhKbSO7IVndgHQAshgHxxtQSrew5gnCkdP3UbNznoKTokQHD7RH2yf3pmK k49icefpJqHfyQw89ZMpy5KWvtudrf07z3tD3jO1zdaJ3A15eI5cqHOrPBwun83ScsHi wzsA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=TQfwU9R8poU4TDXvBFOiAC9Nqmvq3efGrxjDYGbMUgY=; b=UeYQhizZT1f4Yf40ty+3K7tlNOIZZHYZLch2Fy2hvVpH5Vciztd1+SZ3jyzyCoB3kH ULkKNjrIGbQV3EOLv61AMmS2CPhrewsLtS5aMuvb18PIZQLrRj3nzj0SugwKvSd5hMaJ ExxEUbsEFqvKxMCdVZ5N/SxLg5GrU+KXHt01D4NMSsxHqdnzwXxp/LCU8WjctJxzmjJS vpmQY7D+amE5gFJIr5GCLBjMzlTuRNYRrea3loPyHIgqJYQAnMRXIbzMKy0R7UORao5S 5FXwwS9NIEFiVkiJHw97lt7a1/S0gL3pFUUVO3fhV+f4Mp83imHAvn3oiGCOYQYaFQzy AFjA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlEge88Nx2J5W7PjXmPElStj/SQqT/mFt5q+aa1pzNYFXu5V8ClU /G6aK4pas/eHWenM0InTTjc= X-Google-Smtp-Source: AA+uWPyL4+jY+iFh1piysXOuQLWq/r1kids4rGL2H9Et5+fsGaKNo7RyjLkCqvPEK2jT3Rp4nbkRjQ== X-Received: by 2002:aca:eb15:: with SMTP id j21-v6mr966748oih.6.1534602620562; Sat, 18 Aug 2018 07:30:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:389:: with SMTP id 131-v6ls627819oid.22.gmail; Sat, 18 Aug 2018 07:30:20 -0700 (PDT) X-Received: by 2002:aca:de07:: with SMTP id v7-v6mr921091oig.5.1534602620008; Sat, 18 Aug 2018 07:30:20 -0700 (PDT) Date: Sat, 18 Aug 2018 07:30:19 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: Subject: [HoTT] Real Projective space (and other projective spaces too) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_892_1308069758.1534602619406" X-Original-Sender: alizter@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_892_1308069758.1534602619406 Content-Type: multipart/alternative; boundary="----=_Part_893_1582503901.1534602619406" ------=_Part_893_1582503901.1534602619406 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable There are a family of fibrations called "generalised hopf fibrations".=20 For the real hopf fibrations we have: S=E2=81=B0=E2=86=92S=E2=81=BF=E2=86=92=E2=84=9D=E2=84=99=E2=81=BF For the complex (usual) hopf fibrations we have: S=C2=B9=E2=86=92S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=86=92=E2=84=82=E2=84=99= =E2=81=BF For the quarternionic hopf fibrations we have: S=C2=B3=E2=86=92S=E2=81=B4=E2=81=BF=E2=81=BA=C2=B3=E2=86=92=E2=84=8D=E2=84= =99=E2=81=BF And finally (only when n <=3D 2) we have the octionic hopf fibrations: S=E2=81=B7=E2=86=92S=E2=81=B8=E2=81=BF=E2=81=BA=E2=81=B7=E2=86=92=F0=9D=95= =86=E2=84=99=E2=81=BF This screams to me an alternative definition for =E2=84=9D=E2=84=99=E2=81= =BF (and maybe =E2=84=82=E2=84=99=E2=81=BF,...) Inductive RP (n:=E2=84=95) :=3D | map : S=E2=81=BF -> RP n | glue : (x y:S=E2=81=B0) -> map(in x) =3D map(in y) Where in : S=E2=81=B0=E2=86=92S=E2=81=BF is the obvious inclusion map. Now showing that this is equivalent to the usual definition would=20 essentially require a construction of the fibrations they were defined=20 from. This fibration is not so easy however, as we cannot 'cheat' and use= =20 the H-space fibration. Now the main advantage I see with this definition is that it allows the=20 complex, quarterionic etc. projective spaces to be constructed similarly. I= =20 don't think anybody has constructed quarternionic projective space although= =20 it should definitely be doable. the main questions arise when octionic=20 projective space is considered as in classical AT it degernates pretty=20 quickly. (Does this still happen in HoTT, if yes, how so?). Finally a disclaimer, I thought about these whilst traveling and haven't=20 had the time to really put some meat on them. Though hopefully it might=20 strike a chord with anyone who has considered a similar thing. I would love to hear your thoughts and feelings about such things. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_893_1582503901.1534602619406 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
There are a family of fibrations called "general= ised hopf fibrations".

For the real hopf= fibrations we have:
S=E2=81=B0=E2=86=92S=E2=81=BF=E2=86=92=E2=84= =9D=E2=84=99=E2=81=BF
For the complex (usual) hopf fibrations we = have:
S=C2=B9=E2=86=92S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=86=92=E2= =84=82=E2=84=99=E2=81=BF
For the quarternionic hopf fibrations we= have:
S=C2=B3=E2=86=92S=E2=81=B4=E2=81=BF=E2=81=BA=C2=B3=E2=86= =92=E2=84=8D=E2=84=99=E2=81=BF
And finally (only when n <=3D 2= ) we have the octionic hopf fibrations:
S=E2=81=B7=E2=86=92S=E2= =81=B8=E2=81=BF=E2=81=BA=E2=81=B7=E2=86=92=F0=9D=95=86=E2=84=99=E2=81=BF

This screams to me an alternative definition for =E2= =84=9D=E2=84=99=E2=81=BF (and maybe =E2=84=82=E2=84=99=E2=81=BF,...)
<= div>
Inductive RP (n:=E2=84=95) :=3D
=C2=A0 | map : S=E2=81=BF -> RP n
=C2=A0 | = glue : (x y:S=E2=81=B0) -> map(<= /span>in x) =3D map(in y)

Where in : S=E2=81=B0=E2=86=92S=E2=81=BF is the obvious i= nclusion map.

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

Now the main advantage I see with this definition is that it allows t= he 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 octi= onic 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 abou= t such things.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_893_1582503901.1534602619406-- ------=_Part_892_1308069758.1534602619406--