From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBUW44DNQKGQEKSRNBSQ@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-x240.google.com (mail-oi0-x240.google.com [IPv6:2607:f8b0:4003:c06::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 638de3a4 for ; Sat, 18 Aug 2018 14:33:56 +0000 (UTC) Received: by mail-oi0-x240.google.com with SMTP id v4-v6sf9791176oix.2 for ; Sat, 18 Aug 2018 07:33:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Xf3OVXBWwmCS9TixeygbloYyhEKrb9QYRjUlzgwmocg=; b=XSOgFP2/ubr7ay7TMOpaSWpjxcatdk9OkvsRyNSSYlww7syxg9NWtoZwlQp5Yiu0fK Hni0z0xqtWXtEDhiUmvUBk3HD8/rdRDFuBdEaScojEGBn+dl9f0hY0xUWfrj4qzkLv+N 5NnT/Uhj73D3Ocxl/23TCHCLQZcf0J6b2RImnKOPFhe0SZELez6dXVTm5um52WqWThPf AasW3jFTsJ2AHfXbeLTlIbIkKTQytER+seFTIAhysilQ7HE9AlYqfbvMkdZeH54Dly52 8j6C6Tm9Y3NH2z8dxRnzi0pReC9m6wv13rxhPlnR1eL9kB7pkUAH2SjgwEcTq+5PwuPw tEjw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=Xf3OVXBWwmCS9TixeygbloYyhEKrb9QYRjUlzgwmocg=; b=FyImAYhogHVDIEkjdUk9eLszMCVSenHYwEgXvazhTloTOjn33YLE9GZGj9S+fFpC7D tbdEzR1L3kuFW5lJqtOphGupo0nQKgIzkHsbl4BYZeMRWDKARYh6MFG7kQKpTPGrmd74 Vxlgl2WOPYyE38U7ufVJkkErzx9IHPFCjfgb1MJsFqwDTGmu6mujWW3JfvY5XcUZ8Xea lBkk/z3i/t1DUeK4c3FIf7PsZSXSvbd/pphAr0y+ncmOBuPbpLbcrsLmSSPpb9w7/0jn awKKTowtRK3Eqjw9GFANS+hTDV3aqCB7glpb+6wwEetmOzJ//KSVI/NI6twYgggZWQud cSZQ== 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:in-reply-to :references: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=Xf3OVXBWwmCS9TixeygbloYyhEKrb9QYRjUlzgwmocg=; b=Zq1l4wCkkyIkGibtBJalZ+P13LaIVRYZBBhXWR7eUbltB7SLhEa9ZXlygq3A90bNPE SBrleakDWuU667xH1Hllu0ZWemAGtBWYHX3PNcl2GlcuHZdGfmerwBDajcAg8IybhwhZ EP/g7YEQkxjy8jxMr999TvoGKaGSqITroH+kB56UeE7+Lv4J7bffTaBVT2AJN0leY1jU MWWI9ILbqLRkbDIS0haDqBEwxxdMnZtpXpmp6wmVVWiYqx3MpRH1GABOTnTTz+l1Jlv9 5aO9KvWjCsSlFhfb2R5RAgkIJ6EL3FW2mbOXMBrHEW2AqC/ka6fOMH6DAEb4uU0QMyLO lqaA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlG9MTZudGpqsJj21igEkSNR/N/YjIfKK0SRRmqrqkzRQ0MSm7JR OsR3Ftq6umayDU95nqjSC5U= X-Google-Smtp-Source: AA+uWPzZY436Mf+1OE35Os0v/wlXHyx3yif4owtGlTX0jd9n2DlfSNR/EQnsZCPbE93dyduRZXFbiQ== X-Received: by 2002:aca:c6ca:: with SMTP id w193-v6mr952917oif.1.1534602835154; Sat, 18 Aug 2018 07:33:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5096:: with SMTP id e144-v6ls640092oib.14.gmail; Sat, 18 Aug 2018 07:33:54 -0700 (PDT) X-Received: by 2002:aca:f495:: with SMTP id s143-v6mr946829oih.7.1534602834621; Sat, 18 Aug 2018 07:33:54 -0700 (PDT) Date: Sat, 18 Aug 2018 07:33:54 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <0b21b31a-65dd-44ee-8ea7-65921770735d@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Real Projective space (and other projective spaces too) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_943_1521504512.1534602834091" 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_943_1521504512.1534602834091 Content-Type: multipart/alternative; boundary="----=_Part_944_2109563392.1534602834092" ------=_Part_944_2109563392.1534602834092 Content-Type: text/plain; charset="UTF-8" The octionic one doesn't actually work for the projective plane now that I think about it as there is no fibration S^7 -> S^23 -> OP^2 -- 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. ------=_Part_944_2109563392.1534602834092 Content-Type: text/html; charset="UTF-8"
The octionic one doesn't actually work for the projective plane now that I think about it as there is no fibration S^7 -> S^23 -> OP^2

--
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.
------=_Part_944_2109563392.1534602834092-- ------=_Part_943_1521504512.1534602834091--