I looked for an example without universe/El  and found

P(X) ;= 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é

2016-07-22 12:00 GMT+02:00 Andrej Bauer <andrej...@andrej.com>:

> 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
>
> --
> 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.
>