From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.179.10 with SMTP id i10mr8318521pgf.77.1511862035175; Tue, 28 Nov 2017 01:40:35 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.101.97.168 with SMTP id i8ls4314766pgv.7.gmail; Tue, 28 Nov 2017 01:40:33 -0800 (PST) X-Received: by 10.84.177.129 with SMTP id x1mr9436454plb.12.1511862033975; Tue, 28 Nov 2017 01:40:33 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1511862033; cv=none; d=google.com; s=arc-20160816; b=yQN5yKJ+pqRlo1WL/2vh9cGJ/hVpbtutyB7AqR028Upn1CLQx2HpEvrWP/G7kTb1X6 IkR3RFawjgo0FJZGJX91N73f/VvLvxhhiRp/b7avq7BNiMuCyn2Io/DkGaHamSyDfm+8 fmCBNRkT/tTPXtwCeESvS0xpcGslqPBDJ/I/Y5JCIjJTxypi/EYaIm3IMT6o1E8isEs8 kwJ3gBEiDi722YVAH3F9ojVR1bi2B5DzchdeCCsC1MY2BlYfoNgG29jOBDTVAHLJLEY1 PUT6+N62NhqgTPLxJNKWrVJQDA0ezV+ZpTZyezChCYaWZef0UifPLDAX0l6oNFnwM+7E DoCA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=63EZC85kG7zbcZcAHWb1GpXbrULyb8jPXGOmKF0/YE4=; b=upb9zHkadEnvG3daUwZStVV2qiEK+3tGnFiGZS1wtnq0H/pfhajDvIOZcdlJH2FNlc yh4y/2GMheRgb8s4MJLi4mUjV+Hoh9hXzH6IoBVpKzOMdzQN4GON0+Mnx5tKj9stbHQ6 cgZet3LEcJtUVXuyNlpj0CLuLCO4P0GDdLV9dlmVT90K3DhpAGXS1xfS6xAaZEfI8x1G w1jemWtKZoWFpL5GNVc8Xn/dcR9zV0s8Gs7oaG63od5LW7X7fqz4ttgi7WtNOLVPBs6j gh9tXdjUmT6CL2QGI/RVintZY6F9eFW3rMM08BZuWOtWmqzlSMauDnAiCkahAJqvbBcl izeQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=aeE1caf4; spf=neutral (google.com: 2607:f8b0:4002:c05::22c is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Return-Path: Received: from mail-yw0-x22c.google.com (mail-yw0-x22c.google.com. [2607:f8b0:4002:c05::22c]) by gmr-mx.google.com with ESMTPS id i133si277904pgd.1.2017.11.28.01.40.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 28 Nov 2017 01:40:33 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22c is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4002:c05::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=aeE1caf4; spf=neutral (google.com: 2607:f8b0:4002:c05::22c is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-yw0-x22c.google.com with SMTP id q37so12993136ywa.12 for ; Tue, 28 Nov 2017 01:40:33 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :content-transfer-encoding; bh=63EZC85kG7zbcZcAHWb1GpXbrULyb8jPXGOmKF0/YE4=; b=aeE1caf4rkSf3L7pjmtE0i30dy8NbomgxuN8ZznoRjZtQZLRKzZlRcJavuzcW5wQAI rIFYPtND/ERWnDTXA6FecsHbFXR39wqhZPgyXKrW8vr2ZNCczaQmpWS4+qeDvlDvJMwl JouU66joy0ciSkuokiBUPhhK4i/6urVYXW79gl49U/byS2mtR68oaJOy23wXVr28BfAU ert3WPas8enzcQcNhPLwsg+BsOFP8d3vdwQkKnlHtTQEm+bLnLO6mpAqAZz1eKaQYmCH 5DatTDBM3LjtZ0fDbwkLWoy952ba0rPyVOSBLJw0lHuMLyY7iMFbZJYKlUIrlrSRiDBj Uldw== X-Gm-Message-State: AJaThX60WpYVZEUs/6v0dopxRFVCGXUMBqdHTQK8sN0pSJWPvDj7IXpJ Ft46iEps4R+CxeoGJ77ul2AQHWKt/8L0VgIapIDaXA== X-Received: by 10.129.133.129 with SMTP id v123mr26095113ywf.453.1511862033176; Tue, 28 Nov 2017 01:40:33 -0800 (PST) MIME-Version: 1.0 Received: by 10.37.33.2 with HTTP; Tue, 28 Nov 2017 01:40:32 -0800 (PST) X-Originating-IP: [192.76.146.22] In-Reply-To: <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> From: Andrej Bauer Date: Tue, 28 Nov 2017 10:40:32 +0100 Message-ID: Subject: Re: [HoTT] Yet another characterization of univalence To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > If univalence holds, then Id : X -> (X -> U) is an embedding. > > But If the K axiom holds, then again Id : X -> (X -> U) is an embedding. > > And hence there is no hope to deduce univalence from the fact that Id_X i= s > an embedding for every X:U. > > (And, as a side remark, I can't see how to prove that Id_X is an embeddin= g > without using K or univalence.) So you've invented a new axiom? Escardo's axiom: Id : X =E2=86=92 (X =E2=86=92 U) is an embedding. (We could call it Martin's axiom to create lots of confusion.) With kind regards, Andrej