From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDRJR3NGSMPBBLXC4DNQKGQENU4HMJY@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,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-pf1-x43d.google.com (mail-pf1-x43d.google.com [IPv6:2607:f8b0:4864:20::43d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5d745c0f for ; Sat, 18 Aug 2018 14:46:07 +0000 (UTC) Received: by mail-pf1-x43d.google.com with SMTP id x19-v6sf5036318pfh.15 for ; Sat, 18 Aug 2018 07:46:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1534603566; cv=pass; d=google.com; s=arc-20160816; b=VZxm4zFvsM8pv7ObooQ1+Q+KqexpCKVscdRv/4yiwoJs8Ziqo9K7r/10bjIV74O6Pg 8cEJYOXI95joD4VOC+LLvzTyHxqqDbIxcKjpCFh54OroMDNYSrOAxS5H0C/czuj+hMZf +swQsLXtQoj6N/F4JCnA35LDaxVIzj5n+JxjuvK9decvrRog9PgSGQ6RbHQ7WncBuhxk omimjPahSILq3TTiAQM6vf4OPs8LKl77/kMw2fW7KLBoQvxKJnprO00cIaNLeeXBt54e iuew8cVloWsuwwg1x1YLxLBIeUYyvkyW3xCpXesh3GBJDmJkDObPtDHKSWFyYrYZjJZk kIMQ== 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=X3ZUnVkfo9LelP6+o5YF5GkuC1DKecwxuViXrRzefFI=; b=pobeb+cC2sZg4IRGr2Z6YnjL8TyneuaEdy2v7gUktbw2qiJREOf3rMH7bxoRghZeQ5 cTEZDDTPV4ePR+r8tRzBANMYBZRapzmKj5wAI/Bms7gT6IeUUSzEkFfkpsxjvnwwhcRc gaBpV6OPLNeKaQrUCIastQ0MLxosbliYU0ZyrW9wL9HXsAwX3wkKZTQ/SO/qeQ2Pq4iw 3GPP+WCqc+LhZIDMqe0bwu+N7Rz4H+3ujQAMj/pUgiKkM9Kgg8UopLk9COPxer3lU3Qr xJmyKyE9g8/YzbUlRGvxPhwv1SM1nqiIefjpOf0Rs5s1wBKT22pVjOiPwtcdII0eR0MC SXEw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector1-uwo-ca header.b=MkLNIFld; spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.66.112 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=X3ZUnVkfo9LelP6+o5YF5GkuC1DKecwxuViXrRzefFI=; b=lfmmfeXugBsgOnwAMFrYnYpntLF83mUwafNOBI4yT8gFoY7/E7pks3N7dlruZsGmyf DJEAsEPJMv8SfmVPBskfBmDxSn7qeJ0flNIPeBwxeUTypcgVPzDfg97jambTGcqG6aCF lVCFxhpGKRsh09veMA01mq2dFUj8aAM/ux1B4dZO0EOO01i25VdNx8nOqE7gMoGjb5AZ no87Lm30GhAzMnmy+5FxZRuFSC2w9yDE+LXeoIbmbk74DinnGxy1lXEvBWCdEYf+ZpjT ZweL9LFLtueQV4jrFTa1b8hx26VhCcG8RN5pfi6SLfotLW5FxCGCxE9y5h64SLEyMtll NkWA== 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=X3ZUnVkfo9LelP6+o5YF5GkuC1DKecwxuViXrRzefFI=; b=uP/tAaTTXwoBMgObNfhnATgEhELDObXtWFwtsMXN0bjwBIqYdEFafq1SRJlnynorwO 3zjPQmhQU3vlHT3bL13M0ybaCi20OdZTJOmQWnDLpUHHE4I50LwNA1RcCyISxVmsOWfY tHzx9u/yHfoISRn+9hImaxaDRV4eb5qrpx4vlUAkEYa4H/aCeKFLpMaPTmIS1Q6Yrjvu fBD7IMgkn/phaujTdoVzJ0l53PsRF4CbFkytXN1zfdbFC387mR/A5aW9pshAUrX0vd9F l0q6cv0T8teCQnTbm4FNfMQbvEVqSG9oGJQAa+qIS8jSEU1Sw7NSXxISHnZKcCeCfbR7 UHBQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGaaC8noGSMVgrohCQRYvoKpYsDxVgVy7XKN6E+Cu6Zck/qZjMz SCDngH9ewGRUmueAyukhyAM= X-Google-Smtp-Source: AA+uWPw4YZTuXbJLMVzIGIxajrnwTBdWm20mj1UZV/Q+Xch8KNp10mTudeKkk3loXnviuX0qR8lfHA== X-Received: by 2002:a62:b912:: with SMTP id z18-v6mr107588pfe.6.1534603566353; Sat, 18 Aug 2018 07:46:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:a5c8:: with SMTP id t8-v6ls3049360plq.11.gmail; Sat, 18 Aug 2018 07:46:06 -0700 (PDT) X-Received: by 2002:a17:902:6809:: with SMTP id h9-v6mr4848981plk.44.1534603566062; Sat, 18 Aug 2018 07:46:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1534603566; cv=none; d=google.com; s=arc-20160816; b=thEekKDujW7UZXkkCCYys6s1fXEqAK4JQqNTXlXBNQzteREkW4po6uKtxNAz9g7rBw xYsDYiYC1HCAwR6340n5a1lc2Yw43dgsKCVq9Lubp6H60EWt/dOk2cg4ZIJ5o4BsUNP2 187oEmW5O272FEth9TehIMgmYfZRZ/EzGChVTWdApuXWYNdUo1bqHsQXPUPIsg54dr0W c7YOQBUhH8HWpdTbs4oLFC9/RNDQJ2X2og4ooxnqX3gVJgWLS4KB2n6Ddpj8TB5C4xdA FdCTP3PIrO+lGaXHsVHNJaGMc57/QA6+s8edJ7+WFc/U8Y20/TsBci7w1OhLQNA16FcS nGVQ== 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=AftBnnXisM08vlcyjjGnEw6bU0ebk/KOuloEESnAmGw=; b=ii6bErelG/9mEkmQZ9iNiOfDCiysoYl8EM59JpNqfGnbTtJnTBRWqux+S0XVO8wo5Z iffxUZL7sVZBROkMTvtWmSAD+1zF/GdTfDbnLsah3YjOi114ES8702X/AlBm1YQCNfuZ YAEZJ8weVK8lZmUQUAw5kVZqKRdHc0/vkgarR+UOEoGeTPBNH56ZyIis7ppEFOlnD0Tk OHiyVlGZrshcDtb0+WB6Q9wkgLGO0ogcxW2c/0wFJNMqdYpNlN5QkyzugjeLq20qic4Z YsUARe3ktS/UK/Clow5XpYd2kNWob8qQCVVzmpoyQsjMP8D6cxKDtteB91OUCDaRkdHI H7+A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector1-uwo-ca header.b=MkLNIFld; spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.66.112 as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-QB1-obe.outbound.protection.outlook.com (mail-eopbgr660112.outbound.protection.outlook.com. [40.107.66.112]) by gmr-mx.google.com with ESMTPS id v5-v6si164724pgs.2.2018.08.18.07.46.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Sat, 18 Aug 2018 07:46:06 -0700 (PDT) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 40.107.66.112 as permitted sender) client-ip=40.107.66.112; Received: from speedy (99.244.16.206) by YTOPR01MB0634.CANPRD01.PROD.OUTLOOK.COM (2a01:111:e400:c555::10) 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 14:46:03 +0000 Received: by speedy (Postfix, from userid 1000) id 001434C14FB; Sat, 18 Aug 2018 10:45:59 -0400 (EDT) From: Dan Christensen To: Homotopy Type Theory Subject: Re: [HoTT] Real Projective space (and other projective spaces too) In-Reply-To: (Ali Caglayan's message of "Sat, 18 Aug 2018 07:30:19 -0700 (PDT)") References: 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::dVKH2VdeHpNoFMbb:00000000000000000000000000D9FB Date: Sat, 18 Aug 2018 10:45:59 -0400 Message-ID: <874lfrhgwo.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: YTOPR0101CA0001.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:b00:15::14) To YTOPR01MB0634.CANPRD01.PROD.OUTLOOK.COM (2a01:111:e400:c555::10) X-MS-PublicTrafficType: Email X-MS-Office365-Filtering-Correlation-Id: deb3599b-b8a8-4003-37a0-08d6051952bb X-Microsoft-Antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989137)(4534165)(4627221)(201703031133081)(201702281549075)(8990107)(5600074)(711020)(2017052603328)(7153060)(7193020);SRVR:YTOPR01MB0634; X-Microsoft-Exchange-Diagnostics: 1;YTOPR01MB0634;3:k5N5MtWjvjA1DNxYBvNiajmAl4aQnK32nXNK5ZYMriJREo/PJq8aykUpeuzIqZWC4H1NziB7nYf+mMnGpSt9BuHbeEG54Hq/JcTBfbi2AycWPyS/hQG+hkZ+VIAqylJIZYYFbHqC6GtRO4k1MJ1rcNSReNTUy3Slv50ujH/D3wompJzlsO3JBJFplFi35z/MY0/W+pVcDaQiv03bc8gBlqTs6sZ4vMmrmwsGEeQLFDviGSCvg/XBe/bS05zgpcTN;25:xL+p0WlHZFAyDVgD1qPMZpJAf/UcghIQ1a8iuC/86scZeuEgpcUOVdbUXbSQ4lApRwnt2ZtsoecXZQ+9gXph4Q1aIELmWlp5Oy5FD+Wn//bBM/a/jpVXBQ1rtI7qQtKLBjEuj5cNDWfKxgNfg+ikBxr+kdDNHlODIbwgbx/4v+oX4HHekHd/cvrEwh0RFSgj2YQmN//+GA8uXSUhQ+2ul0T7eVreE3bWgAas2KQzJchAPWAMyVewtSqezfsjv6XZ3erkstdkOsMOULFmwb6ndb5Oew4J5CSHf5qLMDmqpgyJ8E5pa7r62XbTqo/0Ecr8brAR8EXgz85JQ1n1J5DHPA==;31:SXLvgU952yQ1wtybbM0jEBbzeBg2ydfDCF2oStsaQERxeIp+Zam5tNxU4WJb9hMxd5M59oKOXS33l6GOeEmb5dugKhtXLg6NE9p5bshM57b5TnsdL84jmT2fKYjQJPrir34dZfH8ZM3IDUzpne8mknU4NzahhjrxvY3CRlsEgyTrRHuOVetkuXtfru/oETs6UZWXbGbRYG2U4Q2+Bq6k7fUDLUMKPpvi2BIZ5TjYuZk= X-MS-TrafficTypeDiagnostic: YTOPR01MB0634: X-Microsoft-Exchange-Diagnostics: 1;YTOPR01MB0634;20:Alobl9mFPF7QjHoel3xLgRys+jJNhIpwpuVNt3b4kuOrHPPCDC9l0/u6PYyz8ezyvXduFgr1QIIM/c+9YghmatI+ZYnJ3tLK8WwV0nK5NcqoUOzvoz7V6aY5alPgR1SuTZOlmqaVfsNr//L1rjU7C4dSHi3bOAkNWKXQRvEc6n/oxfJiXUq3dH/7TjsZNaWW+5wWQIxPWAhE8jkTCFvR5dvk9NpIGKm/xDSaYkIW6OTBsN0iIBdteMbbouEim5a/I+iXB7Uc4SVnPCNK3ZfovFgA9VIIym56MY2cbMOR0lYWF2fZ3kmTBGhR76nSdYYGtw8ZJHTq7XIJP8fS0/iPq7iDNr7mTrxAK3AzQ4aosTH/yNMRJcbAaNbaUDKy1jgB3qUaXvhY1LI58Oj9eNHlF6aHDP7YAWp94bVR42Pzb1pWwoV653wRMPKd3k9HU+1nsX+Gs3tScwnKFgRWto5iL//GwmOyQ6j46rERWZEFfQtOP+uesR7fxkElXrZD6n9A;4:6SdYs5uGQejuOewVJCvnzEdS6Un8ycMy3SanwRePVbpgMRPb1lUdUWXZslNcam1JHgHmOtTcQnu7f0RqqEFkH8pwjRhNgmv7fzu570jPtn+QThIDo1fFjXOiM4oqv3WdedRavJ5xLtcQLpGIiXTjtYtj6W/0fIYvH1SHZunNQu0TNxnBYeU6pdvTgXTZ/rg59LMEULuupNv0DNC3yaR83punos3F9/vUptCGeHiIOtnwJRUFcYbmAivCyyAW0P3YweQQXi3CrVC0DUqvVeeNB57Lhyy19SFYw7ph64wrQvOxgsBZe01F2niIwazUZ0DLmc1/TMJzGbWbXWv9QKNo6IzAA5gS813Ihe1eArPjB6A= X-Microsoft-Antispam-PRVS: X-Exchange-Antispam-Report-Test: UriScan:(127643986962959)(85827821059158); X-MS-Exchange-SenderADCheck: 1 X-Exchange-Antispam-Report-CFA-Test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(93006095)(93001095)(3002001)(10201501046)(3231311)(944501410)(52105095)(149027)(150027)(6041310)(20161123562045)(20161123558120)(20161123560045)(20161123564045)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(201708071742011)(7699016);SRVR:YTOPR01MB0634;BCL:0;PCL:0;RULEID:;SRVR:YTOPR01MB0634; X-Forefront-PRVS: 076804FE30 X-Forefront-Antispam-Report: SFV:NSPM;SFS:(10019020)(396003)(136003)(376002)(39860400002)(366004)(346002)(199004)(189003)(5660300001)(97736004)(316002)(106356001)(786003)(966005)(478600001)(105586002)(42186006)(58126008)(66066001)(47776003)(68736007)(90966002)(50466002)(186003)(86362001)(8676002)(36756003)(74482002)(6266002)(26005)(229853002)(6246003)(486006)(426003)(2616005)(476003)(81156014)(5024004)(81166006)(53936002)(11346002)(446003)(3846002)(7736002)(6306002)(305945005)(52956003)(23676004)(2486003)(6916009)(6116002)(52146003)(8936002)(8746002)(76176011)(2906002)(33896004)(386003)(52116002);DIR:OUT;SFP:1102;SCL:1;SRVR:YTOPR01MB0634;H:speedy;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; Received-SPF: None (protection.outlook.com: uwo.ca does not designate permitted sender hosts) X-Microsoft-Exchange-Diagnostics: =?utf-8?B?MTtZVE9QUjAxTUIwNjM0OzIzOjRxWnk2Q3RHV0lNTStMaE9FZi95czUwRm5w?= =?utf-8?B?Y3ZYSXNBTjBaTk9PSjZNeXc1TVFDaDU4V1RmNFgxd01QaHV6cTBlbTRiakds?= =?utf-8?B?bGgzTjM0eG5iamE0OU9XVFQxdWFLOXBoTURNWEdIUDlpN2VIWGxxSEpjNnZE?= =?utf-8?B?YlAwVzUrcTM3S1cxcGp5WjJMOTV5cEhyVmZySSthZ01mSkdaeURGVzluaWND?= =?utf-8?B?S0ZUVkZDN1NkdGlrYkNZU1o3NlJ6U1V4cmkxbjZ5SHVKMmM3Nkp4QkRmWjdZ?= =?utf-8?B?U05acVNRMDlQbU5CTVpOVG1xNUhvbGl2ejZQNnloRlVYSGlTQzF1Wkhsc0dH?= =?utf-8?B?UWdIcDlYcUE5NWtOaVZwb0lTMzJNSU9DT1poRGJqdlp1QjNNTENwWWR1OEpq?= =?utf-8?B?Tms0ejFOcC9XTytqbzlwZXNudkJiQkpkOHBrZmNnUUd1VUxrelhEZ3k2WTEr?= =?utf-8?B?dk9obEZPYkRqODlFc3pQaUorOUllRkNUN2lUVllKclBRNVhOMGEvdmZnMjgr?= =?utf-8?B?RmtxeTMrSzBzUlMxSWExcnovdFFYcVU5Q0RBcXQ2RThpdDYveUhYNEk4U0ln?= =?utf-8?B?K0toSDFLdGZoYjljVjV4cTVnT1RzcHMwQVdhb001ZVZPYVJKemhZY2JTY1NQ?= =?utf-8?B?Zmw4ZDB2VHhRUEV0UHk5NWVUNEUwNW5XdWN5blJidU1jUXd1UU9JV0R2MTM5?= =?utf-8?B?YmVLR2YxdWRCSnNUTks2eFlPcGcyK21wc01pLzJnUUpYU1FtVERKK3NYQ29y?= =?utf-8?B?SFhmN0Z2RlNvd0NwMkgyVDl0eEVONlF0Y2R1RXFUZUpleWo3M3kyYVpsdUNZ?= =?utf-8?B?YjhOYjV5WDdkdDIwcW9pOUlzMGZtd2NWSWpFbE5mOTlCZ3VWc0RaUklHMXp0?= =?utf-8?B?aEIwRkdVSVdwekV6dDVabmtKL241TTRVTHV1anBIL2xZL0NSMWExbHJuOXZj?= =?utf-8?B?c21zQ2hMTFl3MVpiVmZvVFhSSkdhdjUya0xPdTJWQzdrdzEyTWk2ZmJXMGd3?= =?utf-8?B?RmcrOW1zcDBWemswNHU5WTJCenBkT3ZMRlIvV0N4bVZYcEdWMnAzZ0tyb0dm?= =?utf-8?B?U2xMY3RFamE1WXlCdzAyNUxGaUg5Z1N0N0FwUzJtMUtuaklNcEhSSk9sWkMr?= =?utf-8?B?L0VBQmNLd2NIQTRQRG45Y3RYNnhoRW1PVnB5b1NNb2dwU2pvckFVbmFIdnZq?= =?utf-8?B?UVN3NUZhKzFNQ0NyQ3MzVjA5ditIV09CbmVnSTVGVkVwdkN3R3JpSTZWUmZa?= =?utf-8?B?a2luSTBmODhzcGdnTTEvcUd1Qm96bXlaY1FDM3BJYThEUWN1eHk1Rktsd3px?= =?utf-8?B?M1BPeGlkVWk3Ui9WaVJFVDU4enhwUTB2T2NFOWdDakNwQUZvYnpuRDhUSExz?= =?utf-8?B?MWxLU1lUZkQ0azBVQ09ZRisxZndKL3ArWWdSVEZMMU5tZmxkSVRmemo3cXhI?= =?utf-8?B?REJFQmt1QlBoY0NWVDM5TVpQOGlSdDZzbXduR3QwV2x3VVd1U3ZRc3FmSTMz?= =?utf-8?B?eDZkMTNpTmtqQ2pzU3dmR1prYXMwOFk2US8yVjYvWFNSUzkrUnBUZHJOZnZo?= =?utf-8?B?K29aUjRUemFaa1l3VWhiaUJDZy9UUkp4a3lMcjJZTi9uZkYyT0RvaTJpcmFY?= =?utf-8?B?ZDJuZlZiRVFTQkJLZjNHUklSdnNpdCtrTWMvTUNVZE1Vc2RLTklVeS9Pc0hX?= =?utf-8?B?RnhaMVJoRHFwL2F4SzREVUp1MHdtY3VpcEEzWmlwWDU4Tjd6TTNKZzExbHV2?= =?utf-8?B?T3BsN05LU1JXQWxhdTNyZz09?= X-Microsoft-Antispam-Message-Info: forIDMcKGHHvDJ/DNB/mxNATCbYNBq6j+ytmOWguVZuM5wsPdRnuJXlGdZx/mHXsSL/zLsAJrjPy0/vSqkf7MA7eoTMctXcRxXgoYA2N3N6Z1F6GGtTdvaiBUIfC+B+n5pISKlTxDz72G8DPDq8oCz/jfu7wcqaA/t5xgpYeAtanMgmFS4AoNoIXlZE77VFpFRdJJ447lIcBMmbZCF/axqYDtUCO2AR4N13rfNChHwjGYpVMvcageUesHtYBFWTDpu7TLkfzjI/AcsbnQL7ueAlI5cHkckaP+li2v4cebbmZHmFV5pEI2dUzLzzWJZJodX5CD173HuAa+wBwLLSLX8MhFFbJzQWZtdACBFO9wxM= X-Microsoft-Exchange-Diagnostics: 1;YTOPR01MB0634;6:L/xTQUxK8lfI6eoMQhb6RTb98dYPaNkJkNj4lV4LfQuIkBQ2Ipiu3GT7z+vtbYjQmLhiwb+yGFtR/5E3zdZLM56VduHlesSEMEgLLYzvkqjlXJuZoKEuVpVXlgGMvFokDo/irJX6iiobLUD17w0sA1E/7Ebnt0/Pb++O5HyHd1m8XFpAPbpvDtFQPBnstFHS0AEWwqwivKPnsb53e610bwR3EKqEFLKaE6W32lyuJhLaT42cx3pul/awCrfr/ZyWPzO75a9YEBTrSbzjGnpnXdD9Ib9jFZqCISEzmVIBr37jaYFR0oQBtBLd068c3cpXwVqFRBRfId1aMwYIPp1ao1wKmok+qFfukng/FOt7UlD/BRLHosd50ZQCamZYbPc9xHIGBZibRUe7e/eA+72NFD5DrAKLHAU69LAJ3OXiDJmkis3k4YpBpIiic2LxdgrdwRq8sLnLUCcb7r14PCYOrA==;5:4otalMt3u7hXzsPRzXzm7M4he6ksQ3fwC0D5T9n7pBGkqkOByx0Z4m/NW4T8TrxCnVhthAlhrrkNnHy+C6ZFhq1ubWGewySvXHoQUVOC38QjKZ/3zOP45HPCoP1WudBHGXqu1miqrJzUUPX+brtYCXKMAIyE7weSpnLG/ittNb4=;7:9VovFC1CIdTKebwfbBNlSO1jnar9S1rZIF2G1VTmHzgwtQgT8TN/aYDZvkl+uUFds/qwZomnTM9upMSPyJKhOpVtmgUhtqJbIZnRcmzrr7dBIPTqRsnRhDBV6q1y5gh51zROCMYS57B7mzhVvY5K04HfOsJPQHWK2B4wubcydcXgPwd/nviVjh/5KpxwHddzrfe6tqf1tBOa3Hx6/S9J24MoDYsG/rIE0G4kIqBjb5aCCE/rugv2VQu5pWJFMIzc SpamDiagnosticOutput: 1:99 SpamDiagnosticMetadata: NSPM X-OriginatorOrg: uwo.ca X-MS-Exchange-CrossTenant-OriginalArrivalTime: 18 Aug 2018 14:46:03.9536 (UTC) X-MS-Exchange-CrossTenant-Network-Message-Id: deb3599b-b8a8-4003-37a0-08d6051952bb X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: ad93a64d-ad0d-4ecd-b2fd-e53ce15965be X-MS-Exchange-Transport-CrossTenantHeadersStamped: YTOPR01MB0634 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=MkLNIFld; spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.66.112 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: , 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 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.