From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.5.216 with SMTP id 207mr14227573ywf.6.1473659963865; Sun, 11 Sep 2016 22:59:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.41.71 with SMTP id d65ls10166156otb.16.gmail; Sun, 11 Sep 2016 22:59:23 -0700 (PDT) X-Received: by 10.13.228.66 with SMTP id n63mr15015501ywe.57.1473659963422; Sun, 11 Sep 2016 22:59:23 -0700 (PDT) Return-Path: Received: from mail-qk0-x231.google.com (mail-qk0-x231.google.com. [2607:f8b0:400d:c09::231]) by gmr-mx.google.com with ESMTPS id y77si1260269ywd.7.2016.09.11.22.59.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 11 Sep 2016 22:59:23 -0700 (PDT) Received-SPF: pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::231 as permitted sender) client-ip=2607:f8b0:400d:c09::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::231 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-qk0-x231.google.com with SMTP id h8so44346809qka.1 for ; Sun, 11 Sep 2016 22:59:23 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:references:in-reply-to:from:date:message-id:subject:to; bh=O02vOKSyDrqp+rdW1pm2fIf5dPqAriy39VYOmllKBbY=; b=PnSxr+kYWceW38xZPnVH+/VtrBXKEOUke4rGhWaEOKgYwEKswcWppus2PiHQRl+9Rk 0FBMZ7QC+iyXzMTz6pTHsOjsyWKidN9dSMolo5CzrzQDayGQIomGQo13D2Ejan4VD4/V m6+wQwxnv+o8CKX/wBu7QnasF1D3P7yDjAZlhMSP2SpJAPXIuzJGaX0e2V2eBxv4+y4c gXWccDHIy/XdbIadPoWJdfr3tN/PsV7/01lmX5lV9enVHp1g62O7Cf/fQNLBMFLGEmYM h1YtQASrPul5gBxN8LVYQB6nnXUdgfZUj5vqZJk3afrdR9X36v/s6ctXmvQeHPtKGmI5 tw8g== X-Gm-Message-State: AE9vXwP8jUcL+rU/dxGh7J+jy56E7xxzKT8MbwxipB2vKHESpwjCTWjCmN9nrXnt4DKf3Ta2GnBZ4ZZ/XWmN5g== X-Received: by 10.55.217.2 with SMTP id u2mr18507857qki.246.1473659963194; Sun, 11 Sep 2016 22:59:23 -0700 (PDT) MIME-Version: 1.0 References: <5fb00299-f5c6-c63c-aade-a688ba2e5f4b@googlemail.com> In-Reply-To: From: Jason Gross Date: Mon, 12 Sep 2016 05:59:12 +0000 Message-ID: Subject: Re: [HoTT] Re: Meta-conjecture about MLTT To: Andrew Polonsky , Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a1149aaa0a0452f053c49320d --001a1149aaa0a0452f053c49320d Content-Type: text/plain; charset=UTF-8 I suspect "one of them provably has but the other doesn't" should mean "one of them provably has but the other provably does not have". On Sun, Sep 11, 2016 at 10:20 PM Andrew Polonsky wrote: > The meta-task is to either produce two isomorphic types in an empty >> context, together with a property that one of them provably has but the >> other doesn't, or to show that this is impossible. >> > > What do you mean by a "property", exactly? > > If you mean a type family, e.g., > > X : U |- P(X) : Type > > then a counterexample is > > A = Nat x Bool > B = Bool x Nat > P(X) = Id(U;X,A) > > Cheers, > Andrew > > -- > 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 > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --001a1149aaa0a0452f053c49320d Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I suspect "one of them provably has but the other doesn't" should mean "one= of them provably has but the=C2=A0other pr= ovably does not have".

On Sun, Sep 11, 2016 at 10:20 PM Andrew Polonsky <andrew....@gmail.com> wrote:
The meta-task is to either produce two isomorphic types in = an empty=20
context, together with a property that one of them provably has but the= =20
other doesn't, or to show that this is impossible.

What do you mean by= a "property", exactly?

If you mean a ty= pe family, e.g.,

=C2=A0 =C2=A0 X : U |- =C2=A0P(X)= : Type

then a counterexample is

A =3D Nat x Bool
B =3D Bool x Nat
P(X) =3D Id(U= ;X,A)

Cheers,
Andrew

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--001a1149aaa0a0452f053c49320d--