Re: [HoTT] A small observation on cumulativity and the failure of initiality

[Michael Shulman <shu...@sandiego.edu>]

I prefer my terminology (yes, I think inventing a new word "class" is so bad).
I don't actually reject "term", I use it to mean "derivation of a judgment
\Gamma \vdash A", and I use "type" to mean "derivation of a judgment
\Gamma \vdash type".  That matches the extrinsic usage pretty closely
in practice.
I only phrased it as "there are no terms" to contrast with your "there
are no derivations".

But let's not spam everyone else on this list any more with
discussions about terminology.

On Mon, Oct 16, 2017 at 9:20 AM, Matt Oliveri <atm...@gmail.com> wrote:
> I understand your argument as a good reason to consider intrinsic syntax as
> being more analogous to derivations than to preterms. But still, trying to
> consistently call all those things judgments and derivations, and having
> nothing syntactic called terms or types seems impractical. Like I said, one
> could have opinions about whether (the things I call) intrinsic terms are
> more like preterms or derivations, but my terminology recommendation is not
> dependent on that. The existing papers on intrinsic syntax always seem to
> call them terms, even when they point out that they're a lot like
> derivations.
>
> I realized my terminology proposal didn't include anything convenient for
> the metalanguage types of intrinsic syntax objects. Normally, "judgments"
> would be OK, since that's what they correspond to. But for now I want to
> distinguish them easily from the extrinsic judgments, which involve
> preterms. I'll call them "classes". They are strongly-typed versions of the
> things often called "syntactic classes" or "syntactic categories" in CS. (Of
> course, calling them "categories" here would be super confusing.)
>
> So now let's try out your opening sentence in my terminology:
> [I would rather characterize intrinsic style by saying there are no
> *preterms*: all you have are classes and terms.]
> That's not so bad, is it? I feel like what makes you want to reject the term
> "term" is that you want to emphasize that *preterms* are not involved at
> all.
>
> Anyway, now I think I know what you meant before, about interpreting
> derivations. But I think it wasn't clear, because it sounded like you were
> talking about the usual extrinsic derivations.
>
> On Monday, October 16, 2017 at 11:06:11 AM UTC-4, Michael Shulman wrote:
>>
>> I would rather characterize intrinsic style by saying there are no
>> *terms*: all you have are judgments and derivations.  Look at an
>> inductive-inductive encoding: its meta-language types are the
>> object-language judgments, and its meta-language terms are the
>> object-language derivations.  Some of the judgment forms may be put
>> together out of a context (another judgment) and a type in that
>> context (a third judgment), but not all of them (e.g. not the judgment
>> for "is a context"); and you can also call a derivation a "term", but
>> that could be misleading.  In particular, this perspective makes it
>> more clear that there is a bidirectional version of intrinsic style:
>> the two "directions" become simply two different judgment forms, and
>> the derivations are inductively generated by the bidirectional
>> "typing" rules.