The semantics is the strict equality. > On Jul 22, 2016, at 2:08 PM, Michael Shulman wrote: > > Thanks! I see. > > But I must admit I don't immediately see a use for such a transport > rule (or how to give it any semantics). > > On Fri, Jul 22, 2016 at 7:00 AM, Andrej Bauer wrote: >> 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 := 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. > > -- > 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.