From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.132.202 with SMTP id g193mr156019wmd.24.1512139789967; Fri, 01 Dec 2017 06:49:49 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.193.142 with SMTP id r136ls296989wmf.0.canary-gmail; Fri, 01 Dec 2017 06:49:48 -0800 (PST) X-Received: by 10.28.51.140 with SMTP id z134mr164213wmz.4.1512139788760; Fri, 01 Dec 2017 06:49:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1512139788; cv=none; d=google.com; s=arc-20160816; b=x7jTCz/6e2w+/+ndsinX9PD1SFxGghIQMOmk0oFP4rurRhA2bzXshE8l05UCJSlq4g DaMbRRjuJ+tMKAf14Hca0Dv6rSAZLr/5GqBs90wDbHqehDcMi4PWJ+go4uzgweVnVD72 LIQiUx13E8daXnkQ2d3pZW3+Dj0n5fwHbJxxCfBXZbuQrhRAqnavDeE2wfiDULui1m1T 5T5lLkA6RY5kxvwkk7UebQh1St5FBCjevQ0gJLjiOw91kskupM7hsitEBiUQQ7S61yo6 t4uJ5fqixvfW6KuggPVb9eJhaA8DWzQLoBs8kgrQop36ZXvko46oDgisLOlRIcXqzTq9 Z3+w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :arc-authentication-results; bh=j3JYjrYbL8buG1jE5ZXEyZcs/srX0vtgMPcmYoSQT/Q=; b=ayk3jGhkYP/y7rNtz/d5fjkhWvLhjiU6JGqxiFUFfqZLkFFo8y5jFAL7ooNG+JvkFR 7RZKvdBMDNbnLHakFrg9scUUTBhP+o3xgcPizKBWgsAzkiDUqPr+HD9UlHRQ/Gzhy/rQ NESgx/yihgbwZV8zI/I9k5rQcHiETsedmg0XhjjF0KJUIDhS7YHl37lshWAxtwKhMVgT BbrDRRB1KJzfakWJWosO4gzjvJMD/sqyed5EEJpuZF1QiaufXuQN6b9okfXePq7uwhVr 1pQRxOPu2as/4mNAgpgyVaLgRCfwqKPgtaPYfFgvlIw6VRh2dDtixkrhUhWKbZEAHPsH 8d8w== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id c51si225287wrc.1.2017.12.01.06.49.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 01 Dec 2017 06:49:48 -0800 (PST) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.127] (helo=bham.ac.uk) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1eKmdQ-0000s8-OD for HomotopyT...@googlegroups.com; Fri, 01 Dec 2017 14:49:48 +0000 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1eKmdQ-0007gp-EP for HomotopyT...@googlegroups.com using interface smart1.bham.ac.uk; Fri, 01 Dec 2017 14:49:48 +0000 Received: from dynamic200-210.cs.bham.ac.uk ([147.188.200.210]) by mx1.cs.bham.ac.uk with esmtp (Exim 4.51) id 1eKmdQ-0003gD-Pk for HomotopyT...@googlegroups.com; Fri, 01 Dec 2017 14:49:48 +0000 Subject: Re: [HoTT] Yet another characterization of univalence To: Homotopy Type Theory References: <29b10ce3-682b-437b-bd45-fdf7b2763cec@googlegroups.com> <6570d6a7-2d41-475e-aa7f-b9dc318e74a6@googlegroups.com> From: Martin Escardo Message-ID: <94d6fcf4-7c28-d02c-49d0-455efbc91228@googlemail.com> Date: Fri, 1 Dec 2017 14:49:25 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.5.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes On 29/11/17 21:12, Evan Cavallo wrote: > Maybe this is interesting: assuming funext, if the canonical map Id A B > -> A ≃ B is an embedding for all A,B, then Martin's axiom holds. Since > Id x y is always equivalent to (Π(z:X), Id x z ≃ Id y z), showing that > it is equivalent to Id (Id x) (Id y) can be reduced to showing that the > map Id (Id x) (Id y) -> (Π(z:X), Id x z ≃ Id y z) is an embedding. > > Id A B -> A ≃ B is an embedding both if univalence holds and if axiom K > holds. OK. Here is a further weakening of the hypotheses. It suffices to have funext (again) and that the map idtofun{B}{C} : A=B → (A→B) is left-cancellable (that is, idtofun p = idtofun q → p=q). Univalence gives that this is an embedding, which is stronger than saying that it is left-cancellable. And also K gives that this is an embedding, as Evan said. Here is the proof that these assumptions suffice. To show that Id : X→(X→U) is an embedding, let A : X→U. It suffices to show that the type T := Σ(x:X), Id x = A is a proposition. To this end, it is in turn enough to show that T → isProp T. So let (x₀:X, p₀: Id x = A) : T. Then ap Σ p₀ : Σ(Id x₀) = Σ A, where Σ{X} : (X→U)→U. Because the type Σ(Id x₀) of paths from x₀ is contractible, so is the type Σ A by transport. For x:X arbitrary, we have maps Id x = A (1) → (happly) Π(y:X), Id x y = A x (2) → (induced by idtofun) Π(y:X), Id x y → A x (3) → (evaluate at x and idpath x) A x If funext holds, then the map (1) is left-cancellable because it is an equivalence. The map idtofun : Id x y = A x → (A x y → A x) is left-cancellable by assumption. The induced map (2) is then also left-cancellable assuming funext. The map (3) is an equivalence assuming funext, and hence left-cancellable. Left-cancellable maps are closed under composition, and hence we get a left-cancellable map f x : Id x = A → A x But then also the map g : (Σ(x:X), Id x A) → Σ A defined by g(x,p) = (x, f x p) is left-cancellable (easy to check, in the general form that if f i : B i → C i is a family of left cancellable maps then the map (i,b) ↦ (i,f i b) : Σ B → Σ C is left-cancellable). But for any left-cancellable map into a proposition, its domain is a proposition. Hence (Σ(x:X), Id x A) is a proposition because Σ A, being contractible, is a proposition. This concludes the proof that T → isProp T and hence that Id is an embedding. Martin