From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.206.138 with SMTP id e132mr1555694wmg.5.1473676509864; Mon, 12 Sep 2016 03:35:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.1.169 with SMTP id f41ls488647lji.21.gmail; Mon, 12 Sep 2016 03:35:09 -0700 (PDT) X-Received: by 10.46.0.14 with SMTP id 14mr2459036lja.8.1473676509238; Mon, 12 Sep 2016 03:35:09 -0700 (PDT) Return-Path: Received: from mail-wm0-x22d.google.com (mail-wm0-x22d.google.com. [2a00:1450:400c:c09::22d]) by gmr-mx.google.com with ESMTPS id a126si711855wmd.1.2016.09.12.03.35.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 12 Sep 2016 03:35:09 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::22d as permitted sender) client-ip=2a00:1450:400c:c09::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:400c:c09::22d as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-wm0-x22d.google.com with SMTP id c131so46338806wmh.0 for ; Mon, 12 Sep 2016 03:35:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding; bh=EmWTEdUmqmNCyUoijWdiffwX+79TsGFo5MJjZOvSipE=; b=rdbiO6Haqv48RHVsOE6wirWYk4hPIal2OUkd+QQbpvdeMAC21fXHqhsYBt2qEPPSw2 M3T83wWHFo4gR7J+juZgcT3PT9MSHrg043S7VELKpuLvUhTFx4p77V4tuVgZqyB4ti1o TqdLmGtusBeipPKQoAs3Yx0JUkqmfU5sraeZFzyZBU+Na2G95xrZ5FHiBp45HSWtqwrr HkJRhifN0s39kyTwFuDV1I9Uco49bSi4q/qq7E8xdNeNh72DZrKxxlEojCWdv1q8Sfk5 TXsguBDEFLxtRpEUZR8O3wNsaQ8olUz1e1My2MU02YNu1e1pXfMJLktcHWk5R1jvSmNk +i/Q== X-Gm-Message-State: AE9vXwNAfg7UU2Le8Uvx3mVbID1BrZhSYISersWOCCxJ5/EV6OtjWjU+dyexfbZoaH3U0w== X-Received: by 10.194.85.18 with SMTP id d18mr13993760wjz.43.1473676508700; Mon, 12 Sep 2016 03:35:08 -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 190sm17193225wmk.13.2016.09.12.03.35.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 12 Sep 2016 03:35:07 -0700 (PDT) Subject: Re: [HoTT] Re: Meta-conjecture about MLTT To: HomotopyTypeTheory@googlegroups.com References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> From: Nicolai Kraus Message-ID: <78ae067e-5d2b-3223-b124-4490155cadca@gmail.com> Date: Mon, 12 Sep 2016 11:35:07 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit On 12/09/16 10:55, Andrew Polonsky wrote: > Type theory with reflection rule usually contains the rule equating > all proofs of equality: > > p : Id(A;x,y) > --------------------------- > p == refl : Id(A;x,y) > > If this is admitted, This is a consequence of the equality reflection rule, isn't it? -- Nicolai > then the following modified example works: > > A = Id(U;Bool,Bool) > B = Iso(Bool,Bool) > P(X) = Id(U;A,X) > > Clearly, P(A). Suppose P(B). By equality reflection, A == B : U. > But then, for x : Iso(Bool,Bool), we have x : Id(U;Bool,Bool), whence x == refl. > Since this holds for arbitrary x, we have x==y for arbitrary x,y : > Iso(Bool,Bool), a contradiction. > > Generally, I think any proof that equality reflection is inconsistent > with univalence could be adapted to yield a counterexample as above. > > Cheers, > Andrew >