From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.46.4 with SMTP id j4mr5297884qtd.23.1508166371312; Mon, 16 Oct 2017 08:06:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.55.56.148 with SMTP id f142ls1307988qka.10.gmail; Mon, 16 Oct 2017 08:06:10 -0700 (PDT) X-Received: by 10.237.35.221 with SMTP id k29mr8751811qtc.31.1508166370723; Mon, 16 Oct 2017 08:06:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508166370; cv=none; d=google.com; s=arc-20160816; b=hkfki+tlctSROEOotncmPR55Z9yROQDofqBeI47/VfHxXdUouThVCEeS3v6IXcDMM/ RSW8j0FvuBjcZbni4p2eIFDpUXooVP4yGTzIeLMysauLWgOwz7RdTatfjvVl8a29wKt4 QPxFBvlM6Wd+1yoLFqga6Gcv1hbfl2zOwFE5e126IFebnOzmwRRz5di8l3rjSZ0i/9PH Lb7Iiw4oUu/e6qNRq6NI4Z+i/NSvpUoe8vUbThHtAn/SHl7MkjjnfpBvMkc6cgVs8A/j LaWhWbacavsUFljgIRl/Y3x1LSqkOuP8RqCvdYGwBbLQrtRUf4LWrvHP+2+3bKF/O6y0 KReA== 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=uOYF+4PsnP2fsFMoZK38By4PgSTyydoknaU3pBvaN4U=; b=KagWlehmdMqRV9HZLmv7wzcccxN1DAzJRgCOrtizAre+TitbD0nAIAw8/vi9CHjEX9 JBP1keFL8+GKBiJX8PY7vX7jmsggAjqTG4FZNFWMn7CT6KpNGGbbHwiwVaxJh1O7KNEO Y4JQe/+ieYz4U/DxIKDy1Cxabat23c3fjsw5INuzBSCGDe4rulnAIN4oPse1rWiNLtey WcK8RW+Hv5f9buQ2MEYAYXud4/fvOkVPHG67lvvNgX3rBa3Tj/pSfN4C8sWcmuC5b6fu oVBx/cJLIpcx8K0EBrU9983cgcAC/IOD59mvNHBhw+CUiuxqTvIL1ifduTG1eK4YEzhH W79A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WyZW/VKO; spf=neutral (google.com: 2607:f8b0:400d:c0d::241 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x241.google.com (mail-qt0-x241.google.com. [2607:f8b0:400d:c0d::241]) by gmr-mx.google.com with ESMTPS id f30si373870qtg.5.2017.10.16.08.06.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 08:06:10 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::241 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::241; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WyZW/VKO; spf=neutral (google.com: 2607:f8b0:400d:c0d::241 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x241.google.com with SMTP id 8so32286418qtv.1 for ; Mon, 16 Oct 2017 08:06:10 -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=uOYF+4PsnP2fsFMoZK38By4PgSTyydoknaU3pBvaN4U=; b=WyZW/VKOI0aFdGGo1eiF66EvT7kPRD0a2PSQ0GvTzrTdqkZoM/spfxsnMGaZDkYKpY mcVA5+8zKXWdVPj0NHlE80pOUj78Hz5nLdoLnrGO3UG/3w6xvUJaljjMlKlGbzWvjwlb zUct4jn4XAidmTqO1dpLCv56JmuASgZS2MyThDK71lrJ+G2AS2X5xomMjCG+LH4E9b3G 9UmOb9Lwi9qHUPWDvePsnt3fkIWaDjvhF8vrwNOo22vUM/S1ZF2eUQBlRO80Dq5UWe6w lL1N8PH2eAp1tKduGv6ODURXtMd2ANsLLjd5Kxsu8LsS7/qyv3swhKNhEtfdyuWbpwyv aFWg== X-Gm-Message-State: AMCzsaW+EC3CtEVhBGtoV32hYB1oe561Y/ROq/veLR+AxAHna4SFafRD UjoA+wVpp6FP/nZRhvFdWWg5la7e X-Received: by 10.37.222.195 with SMTP id v186mr573164ybg.486.1508166370115; Mon, 16 Oct 2017 08:06:10 -0700 (PDT) Return-Path: Received: from mail-oi0-f54.google.com (mail-oi0-f54.google.com. [209.85.218.54]) by smtp.gmail.com with ESMTPSA id 11sm625388ywy.96.2017.10.16.08.06.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Oct 2017 08:06:09 -0700 (PDT) Received: by mail-oi0-f54.google.com with SMTP id j126so25581212oib.8 for ; Mon, 16 Oct 2017 08:06:09 -0700 (PDT) X-Received: by 10.157.63.5 with SMTP id m5mr597645otc.125.1508166369076; Mon, 16 Oct 2017 08:06:09 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Mon, 16 Oct 2017 08:05:48 -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 08:05:48 -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 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. On Mon, Oct 16, 2017 at 6:45 AM, Matt Oliveri wrote: > On Monday, October 16, 2017 at 1:10:20 AM UTC-4, Michael Shulman wrote: >> >> What you call "intrinsically typed syntax" is what I favor. I want >> initiality theorems that are proven by a straightforward structural >> induction over something that is inductively generated, and >> derivations are the basic inductively generated object of a deductive >> system. > > > I want to set up some terminology, which we should try to use consistently > for this thread. (I mean Mike and me, but others could follow along too. It > might be helpful.) > > In the extrinsic style of syntax, which is the usual one, there are > "preterms" and "derivations". To notate types, there are either separate > "pretypes", or else pretypes are a subset of the preterms. The thing to the > left of the turnstile is a "precontext". > > In the intrinsic style of syntax, there are contexts, types, and terms. (In > principle, you should be able to make types a subset of terms, but I haven't > seen that, and it doesn't seem appropriate for categorical semantics.) There > may also be other things defined mutually. > > In the intrinsic style, there are no derivations. One could have opinions on > whether intrinsic terms are more like preterms or typing derivations, but > they aren't actually either of those. > > Techniques like bidirectional type checking don't seem to apply to intrinsic > syntax. You don't type check intrinsic syntax; it's intrinsically > well-typed. I'm not sure there's even any analogue of bidirectional > judgments for intrinsic syntax. Maybe you know one. I bring this up because > you were talking about interpreting derivations of bidirectional typing. > That sounds interesting, but it's totally not interpreting intrinsic syntax. > > So you're saying you like intrinsic syntax, and how it lets you interpret > with one structural induction. That makes sense. But that's not interpreting > derivations. If you interpret derivations, then you also have preterms to > worry about, since they are what appear in judgments. > >> It seems most natural to me to introduce terms as a >> convenient 1-dimensional notation for derivations, and departing from >> that is what causes all the problems. > > > What's a 1-dimensional notation? > >> >> On Sun, Oct 15, 2017 at 2:00 PM, Matt Oliveri wrote: >> > In order to assign meanings to derivations, one would have to define >> > derivations. Technically, to assign meanings to derivable terms, one >> > would >> > only need to define derivability. All information needed to pick the >> > right >> > meaning would then need to be included in the terms. This might explain >> > the >> > disagreement over whether unique typing is necessary. In the middle, you >> > could assign meanings to derivable judgments... >> > >> > Given the usual raw-terms-then-derivations approach, interpreting >> > derivations is the most flexible. Gabirel Scherer brought up functor >> > semantics of refinement type systems, which seems to be studying the >> > general >> > situation, with a category of derivation meanings and a category of term >> > meanings, and a functor from the former to the latter. >> > >> > With intrinsically typed syntax--what Thorsten is talking about--there >> > is no >> > separation between terms and derivations in the first place. This is a >> > style >> > of syntax for type systems where--as a design constraint--all "relevant" >> > information is included in the terms. >> > >> > Mike, I'm surprised that you favor interpreting derivations. For a >> > categorical semantics, there is only one "level" of meaning. (Not two, >> > like >> > with a functor.) So I figured you would find it more elegant to stick to >> > systems where the meaning can be assigned to derivable terms. Even when >> > this >> > sort of system is not directly amenable to implementation, it provides >> > an >> > interface to separate syntactic and semantic concerns. >> > >> > On Sunday, October 15, 2017 at 12:00:36 PM UTC-4, Michael Shulman wrote: >> >> >> >> I mean, it seems to me kind of like the difference between proving a >> >> type A is contractible by >> >> >> >> Sigma(a:A) Pi(x:A) (x=a) >> >> >> >> and by >> >> >> >> A x Pi(x y:A) (x=y) >> >> >> >> i.e. not much. But maybe I am missing something? >> >> >> >> On Sun, Oct 15, 2017 at 7:53 AM, Michael Shulman >> >> wrote: >> >> > I'm not saying to do anything different mathematically, just to >> >> > *think* about "using a partial interpretation function on >> >> > prejudgments >> >> > and showing that all derivable judgments get a meaning" as *being a >> >> > way of* "assigning meanings to derivations and showing that distinct >> >> > derivations of the same judgment get the same meaning". >> >> > >> >> > On Sun, Oct 15, 2017 at 6:57 AM, Thomas Streicher >> >> > wrote: >> >> >>> > When writing my thesis in the second half of the 80s I found this >> >> >>> > too >> >> >>> > difficult and instead used an a priori partial interpretation >> >> >>> > function assigning meaning to prejudgements. It was then part of >> >> >>> > the >> >> >>> > correctness theorem that all derivable judgements get assigned a >> >> >>> > meaning. >> >> >>> >> >> >>> Couldn't one consider the latter to be a way of doing the former? >> >> >> >> >> >> In principle yes but it is very laborious. First of all you have to >> >> >> formalize derivations and do a double induction on them which I >> >> >> don't >> >> >> know how to to perform. >> >> >> >> >> >> Thomas > > -- > 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.