From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.0.248 with SMTP id 53mr5841584otk.125.1508171901878; Mon, 16 Oct 2017 09:38:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.63.69 with SMTP id m63ls4187269otc.9.gmail; Mon, 16 Oct 2017 09:38:21 -0700 (PDT) X-Received: by 10.157.81.80 with SMTP id u16mr5499069oti.94.1508171901312; Mon, 16 Oct 2017 09:38:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508171901; cv=none; d=google.com; s=arc-20160816; b=R3475PuCvrCmxr3pVEEIxLqO5DzHjBMUfuLl78SwvN3Y3PK6U94AwAi9HdVj4BbxHg cEU8o0Agtavi8oeM0BZn9S1D/e5c51Nl04wqnMSSmhUfwI458B9viiaoGhFuV295eYt8 eNlcjMNUlZ1s9gQ26tSB3+7/XGVkrdWUd0cuyfDPZg0FBA7fDfZEiEFKq4nml9ce6eyk s1X1teSXhH53RwL9LFzlwym1jkcl/s9atWfeZ+BCvCKpk8bmasvWEFwSoVaFxwD/ltZ3 muHizGMPnCAV2MflLQJuieCa5Qcfj5RL6dhNXHeEK64ZvDIXJmS2okkQurue6MTSDHAb Zz7A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=VeXOhiKH95dxpPiGIeNZFIkMqjaTNWrdedqgdNkjQK0=; b=aWea7jELUnbCi6OWv4e7Vt1j6fbahfyUN/x+Y6w79XlJuIQ0jH4FJniJ5EZXxVpWHI JgjeXkKHT4Su5wGa9nlf96W3oUkmGc4h3MWjPAoC3JT/1TnqchoqWuCvXKVX6qO69ID4 PDcvib/61tnDelCYrEAsgJs6N88Tn7+cNMBSZsrrMAr01flnds1OlAMReYB84RpoI/x8 1X9c9VyMr95Q1zYvrqyGBJbeEGdPE+6t7okmEfMJSfA37jLUZuFyQvxhlOfK2XWRexcF /Jr/QPTIFix1b2sTG5ogcIsPCt/xF1cUH6q1awPbGdkQV4xAFwK2fm09pl6PH2ipf8e8 e3hQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=reAUv1NX; spf=neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x22d.google.com (mail-qt0-x22d.google.com. [2607:f8b0:400d:c0d::22d]) by gmr-mx.google.com with ESMTPS id v33si529762ota.3.2017.10.16.09.38.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 09:38:21 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=reAUv1NX; spf=neutral (google.com: 2607:f8b0:400d:c0d::22d is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x22d.google.com with SMTP id z28so30466498qtz.13 for ; Mon, 16 Oct 2017 09:38:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=VeXOhiKH95dxpPiGIeNZFIkMqjaTNWrdedqgdNkjQK0=; b=reAUv1NXItKHKnADgQpTKFiiJaCcFI234227VV6pwLjyGEmtUzhsWeFCCxzYK+i6wP rT10HWXJ/uFKeWX2mCPGw35x8bdQDH3rVUaXPErIuN3P0FjTaZXE9b6EKbTJrqUEF/pZ 0zhF19y9S1GzggGf6NPpeS7BrAMhpo0CfwpoQUAT+d0+KedMr4/lXeqlX/GvXsgBMk+6 zC0Yp4Fqt/BQwdFqfE8k/PLrCj49zxLeOGfNlJdzlP4wBJZHiueWDuHtHSN+NuCM741U NRMRTBiDFr757CDqbp2DVrbMuB00gRiRXoewvww5L+mbqRV072R41jXI3Jvmn3fo5WIu jp5w== X-Gm-Message-State: AMCzsaU/DiANWESfx4ejMIQY5LF6zHJGNM+ix9qbsJKTsFbCgVLzTXXN Pw//HnJx0ONBtF+KKTjIDhCbY3ff X-Received: by 10.129.233.2 with SMTP id d2mr830663ywm.407.1508171900896; Mon, 16 Oct 2017 09:38:20 -0700 (PDT) Return-Path: Received: from mail-oi0-f47.google.com (mail-oi0-f47.google.com. [209.85.218.47]) by smtp.gmail.com with ESMTPSA id u12sm4667584ywu.93.2017.10.16.09.38.20 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 09:38:20 -0700 (PDT) Received: by mail-oi0-f47.google.com with SMTP id v9so26072333oif.13 for ; Mon, 16 Oct 2017 09:38:20 -0700 (PDT) X-Received: by 10.202.62.198 with SMTP id l189mr5851992oia.281.1508171899920; Mon, 16 Oct 2017 09:38:19 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Mon, 16 Oct 2017 09:37:59 -0700 (PDT) In-Reply-To: References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> <20171015074530.GA29437@mathematik.tu-darmstadt.de> <20171015135740.GA7845@mathematik.tu-darmstadt.de> <37664950-3045-4570-af39-5f44bfc13a1b@googlegroups.com> From: Michael Shulman Date: Mon, 16 Oct 2017 09:37:59 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" 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 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.