From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDRJR3NGSMPBBGPK4HNQKGQEIWHJRCY@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.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-wm0-x23a.google.com (mail-wm0-x23a.google.com [IPv6:2a00:1450:400c:c09::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f44f539a for ; Sat, 18 Aug 2018 19:35:54 +0000 (UTC) Received: by mail-wm0-x23a.google.com with SMTP id f11-v6sf7228065wmc.3 for ; Sat, 18 Aug 2018 12:35:54 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1534620954; cv=pass; d=google.com; s=arc-20160816; b=ThA/C3JHaE12yY/7+mFou1Vp9aMdMIxN/bdG7RD81qnzXYpHNi0b76DENNG9kHur9W qGyXfSaIauf8vZGQivF28bAYWmC3XRl2q4jfjgqko9fhw4V6kauOnuw2/A/MgzkmEwft XqC7/vH01VexXflMsTfwSvWL8LZi0kvrgVywOkiV1qKmYiQ/ahyLgE5nwfp/+4MLFb31 HubPp/ED1JnNiOHtmgoXLVPvg+dhlvoI0OXwhViPbiD32kOqzhiGX7/LY9gyVTX/GcPX +SfgyoKuFAlVJZT0s7Z3IiQsuvpVZ47hVgkhFdFCBVrCrAIjGcjSNGvQQYRbIEzlGcsZ 8Jjg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:spamdiagnosticmetadata:spamdiagnosticoutput :content-transfer-encoding:mime-version:message-id:date :mail-copies-to:user-agent:references:in-reply-to:subject:to:from :arc-authentication-results:arc-message-signature:sender :dkim-signature:arc-authentication-results; bh=vu1KeD4bkTofNZSrDFIXamCrsKZlp6cUaRJJBwwArWw=; b=uweJz0YXkNWxgSuXQyC5llfBNTQ90Rg6NQJCc3L8NXztt5CvQlIyQFyxZZh2XJYq23 AK4exT0oG9MSq9Zsmihz1JW1+xCNRp5uevw/iA9SxeBfJJIliGYrf082qaWVcVdvNS3i kl9LVhLW0rK0te8BSIWbbY2z1oJLExc50MovjmrxkeX+nJIM9/xdfpc6/ks4s4hWp3+k 3m0iDm+ZgpxWiakUI8XBNZ1t3AelPd+ykaVGN5oFUtDx/GcK6IHbg4ApHj3sm6AVP1L7 sfRkyLC/ryZyItZ9MRUvprBmA5zIYvhTQ1z236aDDMekGUOuQj5FtTWMeBOVxDtyOuya bq9Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector1-uwo-ca header.b=ojc0RLFS; spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.67.125 as permitted sender) smtp.mailfrom=jdc@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:in-reply-to:references:user-agent :mail-copies-to:date:message-id:mime-version :content-transfer-encoding:spamdiagnosticoutput :spamdiagnosticmetadata:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=vu1KeD4bkTofNZSrDFIXamCrsKZlp6cUaRJJBwwArWw=; b=c/PQlTxKbh8rRdGNQlZQWC+QJjCvqHlMgppiUDbeZ0dahWOdTGf09nX8bn1r+kzi+K Rug+1Qu4P0D/MuLXSE2UUu2/UQjzmqT4Fl1pPaKgqLDyytDgQNQFETgayFjchZNW2QpW yBuS1ImD55BQJm9eH+dxiuzJPU85PNniMP/uDxuAuK8pIWKG+dQbuPzWl48TdwljQhNd w7sKyo+J3h48JPHmxp3Zz0Eaa6kmd6ntSg64p55yn+zC+6AH8KTCrA5rG0ub8IMj+BPE eaf6tzXYTj+ec22xl4AfNN+MKQxcL/m2kiV8Bw6FdPYWJxpm1dkZCFjgLTIGeFBwl6Qd 93jw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:in-reply-to:references :user-agent:mail-copies-to:date:message-id:mime-version :content-transfer-encoding:spamdiagnosticoutput :spamdiagnosticmetadata:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=vu1KeD4bkTofNZSrDFIXamCrsKZlp6cUaRJJBwwArWw=; b=qpGd0nsmgV3Y3x3GRZsFlmfIsvwCbcj8ZCATcssL4rKIhPQUIWKjoSYkgmodYbM/Ag 1e+8UV5Sjf6ZmXZtnuJBWo+8jvOppX+d5dDszym+01v8EBxJfUxPtJocaNvs7kfHoT7A IwvuTror8ydBjdkf/XCIuduYvyv/PUayI6kva9tS4mf07PxYN2bQOuKZuyGz4Iw/Vkz8 Cc+zUN2P3SIQI3HTeLgVrM/0LGPj1FYuEUsWXaSUzayX5RgFPPFtBJnh1dI2HUihZmx+ +ug52b8eFmI1w3I0+EqVJj1/3kuuIvP5Sid54pLO/g6w+KAb7p3wfDRgPbEVuSP2OAYo FXpg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGpeP+dcLyoJwknjMW7RfBqfQLn3/o7drbk5NCvW50P5wfEuFDn DzPwiZT1EAEv9htVQOFs0Bg= X-Google-Smtp-Source: AA+uWPyNjOFwqvWw5yphQFZI2qeQ3a08xJ0hPwqGCgsahtB4gp32Y9J1EB5lKjfd9X7ZLSc4NGqGBQ== X-Received: by 2002:a1c:f40e:: with SMTP id z14-v6mr215135wma.0.1534620953963; Sat, 18 Aug 2018 12:35:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a7b:c0c8:: with SMTP id s8-v6ls2468984wmh.10.canary-gmail; Sat, 18 Aug 2018 12:35:53 -0700 (PDT) X-Received: by 2002:a1c:7dc7:: with SMTP id y190-v6mr3490929wmc.32.1534620953484; Sat, 18 Aug 2018 12:35:53 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1534620953; cv=none; d=google.com; s=arc-20160816; b=JsnMIrJ+jgUM/W1LYAHRpCg0ehF5623aAGmDzR2RXFm+K294OtTKS8MZfj3aXWjcWZ Z1RkX0bEl6eUS3+MrmeNQFPDIo8TpgZBIsEMmSw/gIPLMi6aDKzWQmSK+6CmUQ5WZdQR brU/TW+/9CgXIlIxCdzqoXMCEgdIwfscC5h9JZh5w2z0H3z2cDywRpiZEMPevjLhbXmn 8wnpYaENbrPqCyodmgyA43kKYQeolqKgK+j9Xstag4xA/Sycvt6nciqVWOKZPRi0FZVO ouOkL3z7cD7nSeg7s4gRLxJj2NPAAFGjhgYkG138NX21yvbHziUXzom1fTHwhCOBunlj Owmg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=spamdiagnosticmetadata:spamdiagnosticoutput :content-transfer-encoding:mime-version:message-id:date :mail-copies-to:user-agent:references:in-reply-to:subject:to:from :dkim-signature:arc-authentication-results; bh=HoxV3FTrr5BwW5LlYKtqWJCaBU0gshfR7zDiIZ+/cII=; b=iK6z1nlR41wLTTxCn0ojSTSGyj5HbzYPWNmXVwS0wduE1xkRXvJ958O6Hiyyhwy34L HU/ESb0s0UW5gsSC4qRhrsCsq84JANzUt6BSNK2BcXwCtye4/ctu0EK0c8REmG72grQC ARk8wbloRAl53Ab0tV3lsauO88Y0I8QZeGwJT5kGjkYhi3VR+e9OvjokXwTMQgErukyk RwuDliXvcHODtzo6dKhIzcKVTlKXf9Cp0JW8QgR1D3aLmEJiNjX9Qp1Cony60IBHlY7c ItrNPMFAZIwNr25zevLZrDYtE1n8W9MxwrA9DBjwpNhB+5+OMJ7hpabkwz7s5DPudtWW ZzBg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector1-uwo-ca header.b=ojc0RLFS; spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.67.125 as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-TO1-obe.outbound.protection.outlook.com (mail-eopbgr670125.outbound.protection.outlook.com. [40.107.67.125]) by gmr-mx.google.com with ESMTPS id p17-v6si176339wrw.0.2018.08.18.12.35.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Sat, 18 Aug 2018 12:35:53 -0700 (PDT) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 40.107.67.125 as permitted sender) client-ip=40.107.67.125; Received: from speedy (99.244.16.206) by YQXPR01MB0632.CANPRD01.PROD.OUTLOOK.COM (2a01:111:e400:5bb8::12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1059.21; Sat, 18 Aug 2018 19:35:50 +0000 Received: by speedy (Postfix, from userid 1000) id BB8924C14FB; Sat, 18 Aug 2018 15:35:46 -0400 (EDT) From: Dan Christensen To: Homotopy Type Theory Subject: Re: [HoTT] Real Projective space (and other projective spaces too) In-Reply-To: (Guillaume Brunerie's message of "Sat, 18 Aug 2018 18:17:52 +0200") References: <874lfrhgwo.fsf@uwo.ca> User-Agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/25.2 (gnu/linux) Mail-Copies-To: never X-Hashcash: 1:24:180818:homotopytypetheory@googlegroups.com::WAjxMMoKgP4RRT3m:00000000000000000000000001q0Ok Date: Sat, 18 Aug 2018 15:35:46 -0400 Message-ID: <87lg93fox9.fsf@uwo.ca> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Originating-IP: [99.244.16.206] X-ClientProxiedBy: YTXPR0101CA0033.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:b00::46) To YQXPR01MB0632.CANPRD01.PROD.OUTLOOK.COM (2a01:111:e400:5bb8::12) X-MS-PublicTrafficType: Email X-MS-Office365-Filtering-Correlation-Id: 2412fbe2-de1a-495e-fa42-08d60541cdfb X-Microsoft-Antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989137)(4534165)(4627221)(201703031133081)(201702281549075)(8990107)(5600074)(711020)(2017052603328)(7153060)(7193020);SRVR:YQXPR01MB0632; X-Microsoft-Exchange-Diagnostics: 1;YQXPR01MB0632;3:sSqE2SJ7pNlh4bkHq0UMjpx4uHH/SLvE3nBEQfjvsZLkth1LvERB2RahLLrFinqRwvcNzWJdmla9iUocwkVcQbOp0ADr3ijWFSSDcTSZXAzcIb5pk++hm8P0BJI/4mnPPN2fUwjqJDpqWHAzazGIS1bAxo75f3d75TQxkuXh4adBO/zIyGN6shFH2ZXOizFsCoHx29Bp+5KzXlZIjLpDvsZHVVYVWYBH20MHy6GzQRu8WA5vQ8b5bMZW2vgyXim7;25:U6+IA7A+bqWWecNNBVBlo/GpBNJ7BQqUfojdbHQkdOfJukQknlmCvruncwox4iCQnOMsHQiz0SQlYQ2fSczr4OlOcJWTaVwpKeaFfV0nIEcsrYPYFkM0kguTsKlgz9sTN9s8eaDnPNQbjmBKeP6oZ0Su6Ka3dhYpAGoXWyW6mZJC9adVdVQfoG107t2cZ/ndDuMlQHWLOezzwLbSSNMfpvL6eBy5nygwpqidFCSCnE4NvbPmsPu5O/VjvqznwgwsIN2u14DePI83T+i9di9PrpZblImHI6rO15uhX8leXInwNsM7JaqQZQRPzSY7pvBYHrRVheXtKjj65CJeZzfonA==;31:eXMseyLmZqc4tpmnkw2t1JpVzHMGZG+5Ml99CkeGiLBdwx1+o2B8ynC2e/W074/cFt/zHKVumrCO0E8Ame4NEWDUkFvGQthEf4loxuG/00rJJLkOFU9aJiLITxpVUH3G4TNizFYm2KNBs4EBfkhZ5gwYcDs4uIL68V6LWOu+vILxtCtuGYh6Vf0aRkvYxyq7qqVUC/YDg4bj8rgNvjr0Xnul/psxKZeo24thYVNN2Bk= X-MS-TrafficTypeDiagnostic: YQXPR01MB0632: X-Microsoft-Exchange-Diagnostics: 1;YQXPR01MB0632;20:JItI07F9gTDKHiuoAdBtWoevZVdZvEo4QJXNitwklBRBi3Fb2Ircwh0BDUWlhtKlZxoDfMFE2vAHyjYqOJHiv5Q6Byl1OqbBW5XYPJcc49WpJA6cRhTWc37g8WFdw0m1dD4A4uVlOPmeKrHsRWqSHnG5IR42QmzjQI1g4Ey11fJl32XOD7NmMu1Blivnn/E3BQ5X96/e2/3vbRwgP7TVnBADyiVzLY3WqmtEuYIJFRnPbu8wBUr+k4xNGtPgrfRBAX10ouXykpQJCtd2csnsL5aG0Ep7bCwksa707WCYaMcGkpXq+FvfjZLbgWfMal1wpfj88h/pnvEvX9isODaa2F/L00DqSd1l+ql929nXy0FOBrbOfCSDXBfli1toeSRUVRU7nRoe+gUct9s+ZW4AHfmcehBzkrebuzrJgbKjd/39KbiYzB21+eNCTfmmJc8L/1b4ucFlhJa/HE4LFDYOBTSPiXk+XuULwLNbA3ZfmO2cGcrb40OlDROLOAqB/vk6 X-Microsoft-Antispam-PRVS: X-Exchange-Antispam-Report-Test: UriScan:(127643986962959)(228788266533470)(85827821059158)(211936372134217)(171883013301213)(95216510686821); X-MS-Exchange-SenderADCheck: 1 X-Exchange-Antispam-Report-CFA-Test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(3231311)(944501410)(52105095)(10201501046)(3002001)(93006095)(93001095)(149027)(150027)(6041310)(20161123562045)(20161123560045)(20161123564045)(20161123558120)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(201708071742011)(7699016);SRVR:YQXPR01MB0632;BCL:0;PCL:0;RULEID:;SRVR:YQXPR01MB0632; X-Microsoft-Exchange-Diagnostics: 1;YQXPR01MB0632;4:FHNKc8SIxpbL4KG7zVnQcB1Qc8KV2in5m3jWTuBgCu/yPT0GgvE2J8NFzAN4vj7y18A6gcGI7Xcn7qfiTKTeRyETMWxKiLkFGWGlZg3y6HGX3K7rr0bMajlBzK6bZ9jj90jDv88rdnKj3ia4yA0A5MCofyeDtoRMlDxR7LjwkILmB7e4sodeO1ShnyZZvK/+zEGckbVjgL/qrTyiuzyo0ac2qg1Q3idLJFwK5iDdOVn4AnSOrfPa33ZUmqQwtvU96+TK4UVcfRghxEHYy8eE38kXMjmnaoY7mpDLZPLSWahkMt19WciT1vEXe33LTinyVgQxB2BHVEXFmcNrNkuzES/3eLHSnpiyx//Ajzl5qcPT5Joff6G0MvMn1sZQt14vIzXdcx7YYfrxs2gNLKZfdg0FPP4vvZBH1RjR9/3wzb27HXiRxad9qLRoV3+Llxu4lruvGRu7oHkTjPeY4faqKXnXQgORTxtajlLt3i32SP0= X-Forefront-PRVS: 076804FE30 X-Forefront-Antispam-Report: SFV:NSPM;SFS:(10019020)(136003)(396003)(376002)(39860400002)(346002)(366004)(189003)(199004)(52146003)(2486003)(446003)(42186006)(11346002)(66066001)(86362001)(52116002)(47776003)(966005)(316002)(786003)(90966002)(6116002)(3846002)(105586002)(106356001)(33896004)(52956003)(426003)(23676004)(6246003)(186003)(76176011)(26005)(2906002)(6266002)(97736004)(81166006)(81156014)(8676002)(58126008)(386003)(8936002)(68736007)(6916009)(305945005)(7736002)(74482002)(53936002)(6306002)(5024004)(8746002)(36756003)(478600001)(50466002)(486006)(476003)(2616005)(229853002)(5660300001);DIR:OUT;SFP:1102;SCL:1;SRVR:YQXPR01MB0632;H:speedy;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; Received-SPF: None (protection.outlook.com: uwo.ca does not designate permitted sender hosts) X-Microsoft-Exchange-Diagnostics: =?utf-8?B?MTtZUVhQUjAxTUIwNjMyOzIzOlNqK1ZJenpBbHZnWjBXbWNXdDcyR0UyT3dv?= =?utf-8?B?TFEwcVd3RTRIbXdydno5bmplZFBTSVBKaTBIQUUvMkhhbkwvZzVhQ0w5US9H?= =?utf-8?B?RHUzK2RxMWdHMWxEdVE4aXFSQ2wvNGozVE91OVB5VE11aExXU2hXUGtDUHRy?= =?utf-8?B?RjR1TzZLUGlXMzZxM2djeWNJYmhhcW1yYWFoZzEvU0Z5WHNiNTFaSERYMjBj?= =?utf-8?B?ajRYSWt5dHJzMTBIOERkZkdWQkJMMmlZS1NzdTZUbjdrOWdSbTg0emZuNVJp?= =?utf-8?B?d1Z4NzJhczhrTDBtL096aVBHYzJPY0Z4RVh1clpyaC95em0rYVlxTzk1QTho?= =?utf-8?B?ZStPcFlob0EwOHRESE16MzZtYStUUDN4RVpMU1F4RXVNVERvNktGUGFSQ2hD?= =?utf-8?B?TWt0YlV1Mkp0S0lmR1hKVEFienlmcEdNOTNIQ3hLbFR1RDlhSExaTkxvK1Va?= =?utf-8?B?REFabWJhYzNIL3JGeW93NWUyMjBVd2M0Q2t1QzBXSStibUl1RjdxMndRMnNq?= =?utf-8?B?K3hzWU56WnNIcXA2UTByYVZ6VzFsSjB1MlZxcUwyVS9WS3FCNFNMb3dvQllM?= =?utf-8?B?dWFRSFh6eWJCd2s0SUpKVFA1N2xRdlFuaWMyWmRQVG9OOFVGa1kyZlY1V1hN?= =?utf-8?B?d2hvdlNjMVdKUG5najVkNTU3UUs5T3NDR0k1dGlBWTkxQ3B5NUhZTE5RTDdW?= =?utf-8?B?a0l4U2h6bFZPMkNoODNpNGsxQXpZT3ZiK1JVdW10dTB2emNxd1dyaW5VajZa?= =?utf-8?B?TDVaM3NXWmhWM3pKOUV1L05KQk1GZllHdEZpRm5qdVJmTDZNbzhuSFpjSGpP?= =?utf-8?B?VWp6WFBsY01yb1ZmdEtnRXBEdGtpTXBIeWU1cHB5U2hYOUZ0aDFtdkltYTFB?= =?utf-8?B?SHJWb2pnVzFzTGdFQ1pWbGlKWlBacFUyYXVwR1gzMk1NbjYzbU9UU2VKM3Q2?= =?utf-8?B?OUFJU1YySHRkWklBcmp3dmJLVThWZnNHRmF0TVZXQ2luaTJyTVIyUng4TUJj?= =?utf-8?B?bXArS2tYZTFDQzVreDQ5clI3Vm01eW5kWTQwNGFGeUlvQmZUS2NpdEpyZjNE?= =?utf-8?B?clY1NDRPZVNMc0o1Q3FaUzU0K0FhV1Jqd3RjVDZ4U3JvZ1NRQ3J6d0JSQW1I?= =?utf-8?B?ZUJPVVlKVFpjV2FoVGxQZHBDKzJkVmJmd2NmcE1pQUtTeCszZFdzZFE0TTI0?= =?utf-8?B?NjlkSEp5ZHRGWU1qblNFNEhtMlcvM2srbk1telNHQmo5VVFQb3d2dUNZa3F0?= =?utf-8?B?aFVtRSsyUng2TXVXZXVTazk3MjRFQ2VnUmlRTFRGWkg5VlpzaGhCbVYvaXQv?= =?utf-8?B?VU81WTI2THJqTlN2T1l3eXYwbG9rQ1ZodW55ZUx2Y2FVWXRjRWMvalMrZVRX?= =?utf-8?B?MFkxZExrbDcxOEkvZ01id2x6MTZ6YjkwWk9KUmMvcG5RcXlNMUlvblJuNEg3?= =?utf-8?B?YWdUREQvQWdBaVkzUjIwcE1NaTR3YW5XUzNETXZlSElzTjdyV2E5NVZXZ1ov?= =?utf-8?B?OVduMEQwM0FvWEIyZkdDTTZ6Y1p5WVlLVXM1czl6RTQwNjFLSEpFMnlXOWpo?= =?utf-8?B?Q1pMcElXZ0dxK3E3Q1pPdjdUZzQ5bitwK2Q1SzNTV3JTTVM4OG93OUdGamlm?= =?utf-8?B?TTl3NjJiMjlMbTd3bG1TNnE5UVVJWGQ0SnpJWDdURHZwMFprU0FVaTlEcDdu?= =?utf-8?B?eWY5MWpOWDMyZzdJSjlKVm01Ymc4M3d6aXhHK2NDYkwvYVppUVkxai9Sc0lj?= =?utf-8?B?M3hXVUZ3VWwxeHJqUVloZz09?= X-Microsoft-Antispam-Message-Info: bOA0xq0/yz4ank1Lcg+YivTjevTaJMHGMGmrbp66hdHCGDC96MR9OOrOi8zcfg5Mpu8UzrMRCp4mbjrN7pgyD+K8POOg4jEu5zKjLua5VoDVAYOLeTWcaW/DuL5Sng6OjcAOhau5STArh4+rbYJsdTZEORiTtWQ77j+x3IdY3qfgtY3nGDvnIbZFTLFzZxgAEHrmQRPSV8pyy1UZrchy2ZweQGTMq0/Y6VPZtUchCWefp6oHVxN4ggaTPl7hRq6z+roYWBzcGGWNOVjbyCMsZ9gLGP7jNTFu31i0rPolXEF0eHtw4Y0FAZoMyYsszt2MWs9P0YqKfACkJq6lekBUeI0up0rjYdJCMFujfzrCIxs= X-Microsoft-Exchange-Diagnostics: 1;YQXPR01MB0632;6:w4Pdpm2Cb6ivjtuTcAoR4692rEJSiVWFR6osX6p0FFpRhPOIYWsxKkoJAuLwoH67+opmus53bCAqww8cRE3McbnZmAb2tt+zqYDZW9GLdxkQPPcJyM3O29FAIFE7BgPUT17o/uMMC4Wb5B/Gmd5ioNXWBvlsi24SXCqHRNZNsWuOYWNkOWEkF98opD19PZJ8NY2j6kv2uWeMqJzC+5eEIXFSWbAgRHP+dTbu/oJyqaz1neXZPOmimhOa1Tqb/ZbdUtjEWixc/otstgApi54lufUy10WlUoIzyrQkhTZ+WfLdC6PpdwlPZY28zyzdEljFpEXoZCd7MiyH3T2QUOnMZwzkgwaUx8hReHxXvjuSCmjfSZkhBx1+5yfRKleto5YSg3kG22M7SLl1ZEurayATOvfdfLbz48QGxatp9JZUJVuMl+XcIN5AkoHr6yrlZykeziq/iqb5vB2TdvnV6Ras9g==;5:wCkf1OqGC8WPky6KNcQjalUX2c9DdyAiOM5iKfMLdnCF7QPjKhpB37adRAfBXjWwqhiLyt6zkcI4liok4/J3qcPd5WlmnlS1s2fNU13CZ0sCZDoWSKDAnRybLEnd7pLU86fy1ZywpH8dJrkyKT1X0BQtjCPdtitfdcMY2eLkTps=;7:+AR8PXT9TXTQQiWG3QKnB3fGSyoGqUAymCtuBxgOXF0N8trd7BTmPkRduW+B+qG4X3zoNU6e44nNN8Dm8d2PMRPS/RjWljfsyUxwCgfH8Wo8eu9PvkBsWn+F/L//b1m+1BR5JGejqhwXVwA37Tim4cfGlhPQSSBWva3UWf4j5J0G5SBVlYA75nsX/vB0Lmqo9/GQCHL2uMSXv9JBYVQ3F00BTaaBMVspOb53EFfrFjizY16CgMt5MBZbke3BVqfX SpamDiagnosticOutput: 1:99 SpamDiagnosticMetadata: NSPM X-OriginatorOrg: uwo.ca X-MS-Exchange-CrossTenant-OriginalArrivalTime: 18 Aug 2018 19:35:50.5989 (UTC) X-MS-Exchange-CrossTenant-Network-Message-Id: 2412fbe2-de1a-495e-fa42-08d60541cdfb X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: ad93a64d-ad0d-4ecd-b2fd-e53ce15965be X-MS-Exchange-Transport-CrossTenantHeadersStamped: YQXPR01MB0632 X-Original-Sender: jdc@uwo.ca X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector1-uwo-ca header.b=ojc0RLFS; spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.67.125 as permitted sender) smtp.mailfrom=jdc@uwo.ca 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: , 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 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=C2=B2 : (x y : S^n) -> glue x y =3D 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.=20 > > Den l=C3=B6r 18 aug. 2018 16:46Dan Christensen skrev: > > On Aug 18, 2018, Ali Caglayan wrote: > > > 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. > > 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 > > --=20 > You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send a= n email to > HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. --=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.