From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.9.212 with SMTP id 203mr1756562ljj.30.1502661922907; Sun, 13 Aug 2017 15:05:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.7.66 with SMTP id i2ls70747ljd.24.gmail; Sun, 13 Aug 2017 15:05:20 -0700 (PDT) X-Received: by 10.25.92.87 with SMTP id q84mr2108881lfb.43.1502661920440; Sun, 13 Aug 2017 15:05:20 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1502661920; cv=none; d=google.com; s=arc-20160816; b=nivIsU1iaGjNc9vd0eUxUSeRobezKtLkLvonWRa074Gk4Y0+fYT6KmY5u1/TuYP/Ez 71TX/+rvSocKLWucSQ4S24paPlkbXSEW9QDMWDqrpZFITaHvazu0KYB+7DOr7CUxf5Yy ncMUA5EblSRskfiM2tP60U20I7WxFPhojshS0HS07IescSuEa/JAFfzCGs5SGqPis9dN Y3vqpaOvEKoTz4hQYSkSo79fJH3qB+wgckysbnDHzBHVtEAY//Nw1LF18qAizbIXEZv2 eBl3u+EVnlbW9VObclVnzbmj24oBDjeyKiANvqZP1Yv+6xhmHBX0L+0HQWzscJPS7xSd 8RLg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature :arc-authentication-results; bh=wDC3oFcQINaDg4eHAZlRH6a+lxRWDd6Rh2g6i/UBpVU=; b=MgEA+wz3Z11ufkCIWPYZY35Di4BKB3e52VQsMmNfIAvIv1Yewe+GfXIOzS2CnrEPpA sYxajmaRqAndkOB0STWqWAxKaH9/s42vf0fWeHSznmy1NmkPsDuEiLIhBTUU5lLJLqi7 uRb6/jFieDm0A2/fE8aKvYUIc1tKSSInXNQooxTFHYaAtGe48fNXX9YD1D8zcKfuyr21 ThjN21TOoqpWYwlryhR/YKkIN6Z4sC1iC1Z7WOSKSlrZ5PnzelzWY4zSXLfw0PlLURO3 leTDIpBOV7gX2/PTa2rxgxZPWm6eLRxndMDp6+nS0pXIfWvSWQsDRMr9R7fNx3MQVwX3 k8gA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=QU2ToWgQ; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm0-x232.google.com (mail-wm0-x232.google.com. [2a00:1450:400c:c09::232]) by gmr-mx.google.com with ESMTPS id r65si240389wmf.2.2017.08.13.15.05.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 13 Aug 2017 15:05:20 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) client-ip=2a00:1450:400c:c09::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=QU2ToWgQ; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::232 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x232.google.com with SMTP id k20so13308592wmg.0 for ; Sun, 13 Aug 2017 15:05:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language; bh=wDC3oFcQINaDg4eHAZlRH6a+lxRWDd6Rh2g6i/UBpVU=; b=QU2ToWgQVSzaQQsA4LxviaiVz1ijxBLyzI8zrMEUgOjYvwZR0Th/eQgECDWNrIpbjW SOv6Rl5Hs9iUa2uz4XnFVj0fDxjyvWFZs7ApWxUMcb6WMYQVbOf4I//8rOJ/V5Zxk1zh Hq0wm5qhfePUJc+UnNIYk8AOEMDpw7oE0I95yaO3LJrgAIgO7Dy472aNoSOb8sq+kMCR bxhVWxe3esmG/uI5HSMvgPH3xXyaMjmOV2sfaS/EwxBxy5pClGRfnC7MBJmW61CMtsai VeL/LQUOK6shXgmKVt0tVvZNKYmc/OHFcptGQEZmrpomiW88Ut4aXbPOBIXM9lERw5+N gQ8Q== X-Gm-Message-State: AHYfb5jNp0PLC/9Qs/z+vOK1A7iibL37dIH2hnTZ7A2kaAYQPB+nld74 h33gDxVw3JRkdpcGeTM= X-Received: by 10.28.182.84 with SMTP id g81mr2943156wmf.100.1502661919563; Sun, 13 Aug 2017 15:05:19 -0700 (PDT) Return-Path: Received: from [192.168.0.2] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id 53sm8438332wry.31.2017.08.13.15.05.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 13 Aug 2017 15:05:18 -0700 (PDT) Subject: Re: [HoTT] univalence without coherent equivalences To: HomotopyTypeTheory@googlegroups.com References: From: Nicolai Kraus Message-ID: <56a8e45f-6800-813b-b70e-c6776dd70869@gmail.com> Date: Sun, 13 Aug 2017 23:05:17 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/alternative; boundary="------------0A7119117811F497A66C7C81" Content-Language: en-US --------------0A7119117811F497A66C7C81 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit I had not looked at this from this angle so far. If you want to avoid having to come up and justify a notion of equivalence, you could, alternatively to ua + uabeta, take the Orton-Pitts "Axioms for univalence" www.cl.cam.ac.uk/~amp12/papers/axiu/axiu.pdf Maybe these are even easier to justify than ua + uabeta! Nicolai On 10/08/17 21:57, Michael Shulman wrote: > Thinking about the recently re-mentioned characterization of > univalence in terms of a map > Equiv A B -> (A = B) > that is only assumed to be a section of the canonical map in the other > direction, it occurred to me that this gives a way to state the > univalence axiom without first needing any "coherent" notion of > equivalence. For at least if we have funext to start with, then > equalities in Equiv A B are (for any coherent definition of Equiv A B) > equivalent to equalities in A -> B, so we can state the retraction > property in terms of those. > > More precisely, let > coe : (A = B) -> A -> B > be coercion along an equality, and let > QInv A B := Sigma(f:A->B) Sigma(g:B->A) ( (Pi(x:A) g(f(x)) = x) > \times (Pi(y:B) f(g(y))=y) ) > be the type of quasi-invertible functions (incoherent equivalences). > We know that it is inconsistent to ask that the map (A = B) -> QInv A > B induced by coe is quasi-invertible. But suppose we instead ask for > just > ua : QInv A B -> (A = B) > and > uabeta : Pi((f,g,a,b) : QInv A B) Pi(a:A), coe (ua (f,g,a,b)) a = f(a) > If full univalence holds, then such functions certainly exist, since > any quasi-inverse can be improved to a coherent equivalence. But > conversely, if we assume funext to start with, then the full > univalence axiom can be proven from this ua and uabeta. (I just > formalized this in Coq to be sure.) > > Maybe other people have already observed this, but I don't think I > noticed it before. It means that we don't need to invent or motivate > a coherent notion of equivalence before stating (or, in cubical type > theory or a semantic model, proving) univalence. Instead we can state > univalence in this way, and then (having already motivated funext, > which is much easier, and also has a "weak improves to strong" > theorem) motivate the search for a "good" definition of Equiv A B as > "can we define more explicitly a type that is equivalent to A = B"? > > Mike > --------------0A7119117811F497A66C7C81 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 7bit I had not looked at this from this angle so far. If you want to avoid having to come up and justify a notion of equivalence, you could, alternatively to ua + uabeta, take the Orton-Pitts "Axioms for univalence"
www.cl.cam.ac.uk/~amp12/papers/axiu/axiu.pdf
Maybe these are even easier to justify than ua + uabeta!
Nicolai

On 10/08/17 21:57, Michael Shulman wrote:
Thinking about the recently re-mentioned characterization of
univalence in terms of a map
  Equiv A B -> (A = B)
that is only assumed to be a section of the canonical map in the other
direction, it occurred to me that this gives a way to state the
univalence axiom without first needing any "coherent" notion of
equivalence.  For at least if we have funext to start with, then
equalities in Equiv A B are (for any coherent definition of Equiv A B)
equivalent to equalities in A -> B, so we can state the retraction
property in terms of those.

More precisely, let
  coe : (A = B) -> A -> B
be coercion along an equality, and let
  QInv A B := Sigma(f:A->B) Sigma(g:B->A) ( (Pi(x:A) g(f(x)) = x)
\times (Pi(y:B) f(g(y))=y) )
be the type of quasi-invertible functions (incoherent equivalences).
We know that it is inconsistent to ask that the map (A = B) -> QInv A
B induced by coe is quasi-invertible.  But suppose we instead ask for
just
  ua : QInv A B -> (A = B)
and
  uabeta : Pi((f,g,a,b) : QInv A B) Pi(a:A), coe (ua (f,g,a,b)) a = f(a)
If full univalence holds, then such functions certainly exist, since
any quasi-inverse can be improved to a coherent equivalence.  But
conversely, if we assume funext to start with, then the full
univalence axiom can be proven from this ua and uabeta.  (I just
formalized this in Coq to be sure.)

Maybe other people have already observed this, but I don't think I
noticed it before.  It means that we don't need to invent or motivate
a coherent notion of equivalence before stating (or, in cubical type
theory or a semantic model, proving) univalence.  Instead we can state
univalence in this way, and then (having already motivated funext,
which is much easier, and also has a "weak improves to strong"
theorem) motivate the search for a "good" definition of Equiv A B as
"can we define more explicitly a type that is equivalent to A = B"?

Mike

--------------0A7119117811F497A66C7C81--