From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.20.142 with SMTP id d14mr4861684ote.93.1508130620797; Sun, 15 Oct 2017 22:10:20 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.202.91.130 with SMTP id p124ls1963992oib.0.gmail; Sun, 15 Oct 2017 22:10:19 -0700 (PDT) X-Received: by 10.157.14.116 with SMTP id n49mr4686689otd.111.1508130619967; Sun, 15 Oct 2017 22:10:19 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508130619; cv=none; d=google.com; s=arc-20160816; b=BingQerDOIIRbUaqRIlv2c/zogbd4NkeeT4IN61oIHWsIU+rzqZQgqJiJCBUcDGpAl NGkOHT8VNZW6C+acLVpy94vT04ZhMKeCv8Mcbj5J3+wOVhktdZjAKV+rJz9Ye0L3rwtK N0nci8DidktHO+YWzz1D3asJ7z5rUV37Ehi5xiSswjTxL4daoV7ZZZlqzxY2ePoiQ4VD /txU4I0Suy0ULf1jBBPmhWUZ93p0GXzzr8qJkSsYb+Qcp+6xSVXTyCnOT/mwgc/G1s5P jgXVpyy65GQgjb6IVTKUC2nAZpyNTfRiOciOp07bnBuYOsKMawRxbVv8yykiAZ37sePS biUA== 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=Mz5YvCqY3yKkn+WbriJiL6F9wZjY9uq6iuLRyQW3i1A=; b=UaneNYgCQmCSouYuamaxEKwMnDKL/+YXSrEn3tCz43+HrYwPYanH3ACo6YJTzybdFp FPfjNE2fFdLT5thaPeTr1UModIREe41NisiB2gbW0+V58u7OxmEBulb4GIkUO6m9kpBt 1MaZHzA2AXEIKysvYc5bKWWqjcjNtGG8wga8KDp/5w6RBSg25eNJIUphB7Zv0iQDDLCg H2g2vJO9VUwvW96oWFu4ILt6ID9RtkzC7zmzchm1p0aZNn88uW71wHkdOm5lZRwkZDuU sZncvyY/20c1P/iCAfcslmaCXSht+Lq7vFMU1XAqGcvwTm6+TzPyW3AK0Tc5kvgSy+6X MNRg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=NWLb4pFg; spf=neutral (google.com: 2607:f8b0:400d:c0d::235 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x235.google.com (mail-qt0-x235.google.com. [2607:f8b0:400d:c0d::235]) by gmr-mx.google.com with ESMTPS id f22si353847oth.2.2017.10.15.22.10.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 22:10:19 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::235 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::235; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=NWLb4pFg; spf=neutral (google.com: 2607:f8b0:400d:c0d::235 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x235.google.com with SMTP id n61so29305119qte.10 for ; Sun, 15 Oct 2017 22:10:19 -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=Mz5YvCqY3yKkn+WbriJiL6F9wZjY9uq6iuLRyQW3i1A=; b=NWLb4pFgOVTPqnnJf8lunJnUEPrJOYMa3WAmuiM+Xx45KqaeGiEQAuK7+flPx8Um/w GdNsKt+B0RwCLmMXljGP1Mkl9qhFz8W6iNl5T2Fx/nR3x+YDi52fbClJcbq4+PBHJefR khqt353flr4qqvC/cy/BclPsN3BgH00fu8rQ6QdU8h7ltAI6JLUv240XojgXtI5pO4j6 L6zfFsPQg2MnsGS8ZwwC5scCFJY4jNVgZycS02Yi9nMg051mVezJOHuJTno0oN8Gpgux Nc/7F2EGFJFHAc2xPz2w71WWnbmdAUga0tJCfdOon8WO6/DsjhzTU5mZIK2dEu2m0dM8 bKxQ== X-Gm-Message-State: AMCzsaUtALycgcbHLsl0p6GT+wJH/fzk7ENKgplsvC8ohF6xWIxgW3s7 NivlwRGKZcSsSgQwajYtsItac8pF X-Received: by 10.129.71.11 with SMTP id u11mr1570499ywa.86.1508130619453; Sun, 15 Oct 2017 22:10:19 -0700 (PDT) Return-Path: Received: from mail-oi0-f52.google.com (mail-oi0-f52.google.com. [209.85.218.52]) by smtp.gmail.com with ESMTPSA id x185sm3368112ywa.73.2017.10.15.22.10.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 22:10:18 -0700 (PDT) Received: by mail-oi0-f52.google.com with SMTP id v132so23399425oie.1 for ; Sun, 15 Oct 2017 22:10:18 -0700 (PDT) X-Received: by 10.202.178.133 with SMTP id b127mr2806600oif.261.1508130617843; Sun, 15 Oct 2017 22:10:17 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Sun, 15 Oct 2017 22:09:56 -0700 (PDT) In-Reply-To: <37664950-3045-4570-af39-5f44bfc13a1b@googlegroups.com> 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: Sun, 15 Oct 2017 22:09:56 -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" 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. 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. 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.