From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.154.1 with SMTP id c1mr2581588wme.2.1469190181281; Fri, 22 Jul 2016 05:23:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.5.193 with SMTP id 184ls286618ljf.20.gmail; Fri, 22 Jul 2016 05:23:00 -0700 (PDT) X-Received: by 10.25.42.197 with SMTP id q188mr635323lfq.7.1469190180498; Fri, 22 Jul 2016 05:23:00 -0700 (PDT) Return-Path: Received: from mail-wm0-x243.google.com (mail-wm0-x243.google.com. [2a00:1450:400c:c09::243]) by gmr-mx.google.com with ESMTPS id o10si490841wme.0.2016.07.22.05.23.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 22 Jul 2016 05:23:00 -0700 (PDT) Received-SPF: pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) client-ip=2a00:1450:400c:c09::243; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of mphm...@gmail.com designates 2a00:1450:400c:c09::243 as permitted sender) smtp.mailfrom=mphm...@gmail.com Received: by mail-wm0-x243.google.com with SMTP id o80so5991090wme.0 for ; Fri, 22 Jul 2016 05:23:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc; bh=T+rcIrtN1A+cz9QJxPSamcpZyef/Pvih1jc6c8zLq1I=; b=NknrZkz5UdA4+fLuR2U+6CLGGoXhHipbcZujTCEEjlL8DLw0lls/VD4Tv7laoETp4L 32CBEixZiUG0ZIY5V6nRjFlXtK7SePbxA/DyZOIkxv5gFfGdA4DuOgcsBmMiqjp4KqQf ukD9xCqncjgVatFpnr4cIznmWikbzZFVwnyaCmg87EPkOluVTOVoOZk5M99tLVbuGj8A SinO79XuxuAijlFOaMd8pwXN5rh7V1/3d6703ifqgpKnUWD7jnKtfEIUw2JatrK5TYKj G2RU8Dq0c4BYpQNFGltGV6ZKBIOAO8WW2lQbyDeYk8us+PJHcXlwibWnAOWnKs7nCTjq tIVQ== X-Gm-Message-State: ALyK8tLePCQFUH2vs98JxSIlOQiik+vMIvjyCg49llbL51xgaxdKo3SC11QM7H4bjuNbqZkltXuCqSn55aEyug== X-Received: by 10.28.31.147 with SMTP id f141mr23649189wmf.69.1469190179373; Fri, 22 Jul 2016 05:22:59 -0700 (PDT) MIME-Version: 1.0 Sender: mphm...@gmail.com Received: by 10.194.133.5 with HTTP; Fri, 22 Jul 2016 05:22:40 -0700 (PDT) In-Reply-To: References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> From: =?UTF-8?Q?andr=C3=A9_hirschowitz?= Date: Fri, 22 Jul 2016 14:22:40 +0200 Message-ID: Subject: Re: [HoTT] a new transport rule To: Andrej Bauer Cc: Michael Shulman , Vladimir Voevodsky , Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a114bddfebfc8220538387eb3 --001a114bddfebfc8220538387eb3 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I looked for an example without universe/El and found P(X) ;=3D forall p: Id X a, Id p (refl a). It seems that the formula must involve a "type from term constructor" (here Id, or there El). andr=C3=A9 2016-07-22 12:00 GMT+02:00 Andrej Bauer : > On Wed, Jul 20, 2016 at 11:10 AM, Michael Shulman > wrote: > > Can you give an example of such a P which becomes well-formed when A > > and B are substituted for X but is not well-formed with X as a > > variable? > > Let > > T :=3D Universe > > nat : Universe > Nat type > El nat =3D Nat > 42 : Nat > > P(X) :=3D Id (El X) 42 42 > > Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes= : > > T :=3D bool > > P(X) :=3D Id (match X with true =3D> Nat | false =3D> (Nat -> Nat) end)= 42 42 > > Now P(true) is well formed, but P(X) is not. > > With kind regards, > > Andrej > > -- > 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. > --001a114bddfebfc8220538387eb3 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I looked for an example without universe/El=C2= =A0 and found

P(X) ;=3D forall p: Id X a, Id p (refl a).
It seems that the formula must involve a "type from term = constructor"
(here Id, or there El).

andr= =C3=A9

2= 016-07-22 12:00 GMT+02:00 Andrej Bauer <andrej...@andrej.com>:
On Wed, Jul 20, 20= 16 at 11:10 AM, Michael Shulman <= shu...@sandiego.edu> wrote:
> Can you give an example of such a P which becomes well-formed when A > and B are substituted for X but is not well-formed with X as a
> variable?

Let

=C2=A0T :=3D Universe

=C2=A0 nat : Universe
=C2=A0 Nat type
=C2=A0 El nat =3D Nat
=C2=A0 42 : Nat

=C2=A0P(X) :=3D Id (El X) 42 42

Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes:<= br>
=C2=A0T :=3D bool

=C2=A0 P(X) :=3D Id (match X with true =3D> Nat | false =3D> (Nat -&g= t; Nat) end) 42 42

Now P(true) is well formed, but P(X) is not.

With kind regards,

Andrej

--
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 HomotopyTyp= eThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a114bddfebfc8220538387eb3--