From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.31.185.16 with SMTP id j16mr2720118vkf.2.1469181627306;
        Fri, 22 Jul 2016 03:00:27 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.157.7.230 with SMTP id 93ls2659228oto.22.gmail; Fri, 22 Jul
 2016 03:00:26 -0700 (PDT)
X-Received: by 10.200.56.7 with SMTP id q7mr2771734qtb.10.1469181626450;
        Fri, 22 Jul 2016 03:00:26 -0700 (PDT)
Return-Path: <andrej...@andrej.com>
Received: from mail-qt0-x233.google.com (mail-qt0-x233.google.com. [2607:f8b0:400d:c0d::233])
        by gmr-mx.google.com with ESMTPS id d6si678224ywd.4.2016.07.22.03.00.26
        for <homotopyt...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Fri, 22 Jul 2016 03:00:26 -0700 (PDT)
Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::233 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:400d:c0d::233;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@andrej-com.20150623.gappssmtp.com;
       spf=neutral (google.com: 2607:f8b0:400d:c0d::233 is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com
Received: by mail-qt0-x233.google.com with SMTP id u25so58770144qtb.1
        for <homotopyt...@googlegroups.com>; Fri, 22 Jul 2016 03:00:26 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=andrej-com.20150623.gappssmtp.com; s=20150623;
        h=mime-version:in-reply-to:references:from:date:message-id:subject:to
         :cc;
        bh=wosUxdQ6DCCyt5DD639/JQKJDGHDENRdo0oc0NMNqUQ=;
        b=ou0PCglGADMMAmLIYnCeRFqJVd/3ZQ7DT66zg/3wYSbl6NZc+Pp7Jy4Lk9oUPaF6FY
         J68y0h4iH4QzBrKCfHAUJ5rgeaxFizp25/UQbKN+C0Eq7gccFW4SVXCi/9eJZwgO3Lyv
         e9CTnknKqpVZUzBYXotO3AFzZpXjQ0kbvGkYWhpUcUM2k5xfrf7mBt4ogAcvmnP+Y1UV
         1EGR9Os9IUZ71Oge6kDfhdQodgYMdD/fbx+ztotTw2p8sCAz/nC5ESSCSyvaRycex4J0
         xMe9PQlCXgQpYGBRVK09kGXooAni3xer5qGmoh11QGDfQ81mH/BhpJcFAGHCyp7J7TQj
         uXzg==
X-Gm-Message-State: AEkoouvAkqLtLSKsEF3X9Y9tDJoX9IyRFGSCl4/pTjwNUlUjlri2nwTOUKtly0kr7SQr5K1rrmvTOC6uQ8pi5g==
X-Received: by 10.200.42.69 with SMTP id l5mr4647089qtl.13.1469181625958; Fri,
 22 Jul 2016 03:00:25 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.55.31.38 with HTTP; Fri, 22 Jul 2016 03:00:25 -0700 (PDT)
In-Reply-To: <CAOvivQxUyau-O=SDZy4ho+EmnFez25_9n67jwjsNGjJ02ypsiA@mail.gmail.com>
References: <319FEA26-A1A5-42F2-9539-8B4635BFC016@ias.edu> <CAOvivQzp+s7fK2NgeFO0fKpWC1OyMibd81vWpZ=2inmdSJu43Q@mail.gmail.com>
 <EB3CE28E-4C7A-465E-A701-8FFE13824531@ias.edu> <CAOvivQzVVOxSoNZKMHqLSyZK06cShetYsxTNmkJGW141Snpf4Q@mail.gmail.com>
 <7DACC421-37E7-43CC-B61F-D6C5F99921DF@ias.edu> <CAOvivQzSs5=e=EEfP42nmDJUogkx7TjrAtYJqAEOFHetcPSZtA@mail.gmail.com>
 <1B8618C8-0499-4D96-BACF-9AA4623061B9@ias.edu> <CAOvivQzg_saqj7re-OCTFUFJceKab_eBR+X+OckFYe6fmkuVsQ@mail.gmail.com>
 <1EE3DCAA-5777-4563-9B54-31D1BAD91450@ias.edu> <CAOvivQxUyau-O=SDZy4ho+EmnFez25_9n67jwjsNGjJ02ypsiA@mail.gmail.com>
From: Andrej Bauer <andrej...@andrej.com>
Date: Fri, 22 Jul 2016 12:00:25 +0200
Message-ID: <CAB0nkh2CmqucrGS2+QS0Yq9OYJCgW6-z8fRkn1JmO0kFVNh+Kg@mail.gmail.com>
Subject: Re: [HoTT] a new transport rule
To: Michael Shulman <shu...@sandiego.edu>
Cc: Vladimir Voevodsky <vlad...@ias.edu>, 
	Homotopy Type Theory <homotopyt...@googlegroups.com>
Content-Type: text/plain; charset=UTF-8

On Wed, Jul 20, 2016 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

 T := Universe

  nat : Universe
  Nat type
  El nat = Nat
  42 : Nat

 P(X) := Id (El X) 42 42

Then P(nat) is well-formed, but P(X) is not. Or, if you dislike universes:

 T := bool

  P(X) := Id (match X with true => Nat | false => (Nat -> Nat) end) 42 42

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

With kind regards,

Andrej