From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.217.204 with SMTP id b195mr4708746ywe.7.1508079257351; Sun, 15 Oct 2017 07:54:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.237.4 with SMTP id w4ls763026ywe.19.gmail; Sun, 15 Oct 2017 07:54:16 -0700 (PDT) X-Received: by 10.129.48.201 with SMTP id w192mr4464053yww.22.1508079256585; Sun, 15 Oct 2017 07:54:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508079256; cv=none; d=google.com; s=arc-20160816; b=tLluzMgrqnNamlIIkGfeJ4JMUOuNNUB9zu1JYEsa6ntCnonJSszKqcz924ryE/qtzM 54y/mtGAUGKJEVntRCyUlSSSjPv4J4Y3J53zsAVbkRlKI2q3e4MoUmq7G9HgHwUEilMS yIlHcpPupASY1oNJJOWKtvzF+G5aHVJOkRXdkEZlluhjVWAsnfHai96FO+JiKtSevpSe ne3OHtnM0fkQKGQvhKf6YAO5/nr/ejThi2NGvoJf65PqfwXErwPzCqF8uA2DxEqXS6P2 tXltUqwlNlzChqsI5O7etkyA+lbBSmZCKXV7iKuQAelMuxhbArbl6SOxQdNlL8T4GFl2 lXsg== 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=PGFtoT6pHdRrKdqqqUkkD6+dHu3F0qeFW1Nf+u+uWwk=; b=drn0QfqJq/GTDMmrYQJ/daxkLDY5Bhq5hiRFtfD4xePFa8nElcXlNvPGVhVBwc5xIO KNWefLnNFOfjC1tUyvBlq9BlTmJhGe+PkW1OXaF1b0scHyqodofJ+iu8fL31iqpdnb/U gcIsuFaoZEr7aM96LuSf74E7Lp8QbYB+VxyCYYZ8EiTzHP3Z24u7A1Y84TO3M4WlrFz1 WXHeHW0veToJmP/4ho7RSqzVCmrMKkNEN6w3hTXmZH0vKS6cQXmUtV6awy+aEJMZomNe dU1jJDxZ3u7EgBDpMxedPZx3MZD2ITbOYrKP7y3pIspS2ihnTP59eZk29Z0rtvvygXCY wnJQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ONLu9k5g; spf=neutral (google.com: 2607:f8b0:400d:c0d::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x22a.google.com (mail-qt0-x22a.google.com. [2607:f8b0:400d:c0d::22a]) by gmr-mx.google.com with ESMTPS id g13si310383ybk.3.2017.10.15.07.54.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 07:54:16 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22a is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ONLu9k5g; spf=neutral (google.com: 2607:f8b0:400d:c0d::22a is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x22a.google.com with SMTP id 8so27304625qtv.1 for ; Sun, 15 Oct 2017 07:54:16 -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=PGFtoT6pHdRrKdqqqUkkD6+dHu3F0qeFW1Nf+u+uWwk=; b=ONLu9k5gFRd0AyYT1kgnpqiYuNhPNSKIdc53w7NLiVFwzVcDRDpCpnc9QY3Mipa5fs 0WTN02uUDYC0B8vO336eaG1Zzb2QM0jbVIM4g0TITcThGgxBvhDz3miM5QE7+poBB3aO m7Ai4Hor1rfkAtFiGzmbp3wTsvYPOdRG5Hf7WYP6aehrLaQ+K+xdmSPkdq2mHEFTqvSF Hicwd2cC2om477F/2jmFpppCu1BPE572cLKr/QlRjPlCN6jDpiBuxZN8cfQ3qf6TWQy9 yCU78Cm/7F/KbEgQSVZ8akOwyVjLBacflr1fG1+G/Bg2JU3x10rAF8P5mwZP4dDmxcaO O9Qw== X-Gm-Message-State: AMCzsaUFLt4htnFv+FWr3BSM5wjU4csPQDCx5o7/gi+IFvG2qOlFxxq+ drhtlz+1G/oYjixO1XuP9qp1vlrq X-Received: by 10.13.254.68 with SMTP id o65mr4451759ywf.355.1508079256113; Sun, 15 Oct 2017 07:54:16 -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 r11sm2591820ywr.13.2017.10.15.07.54.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Oct 2017 07:54:15 -0700 (PDT) Received: by mail-oi0-f47.google.com with SMTP id h200so21196981oib.4 for ; Sun, 15 Oct 2017 07:54:15 -0700 (PDT) X-Received: by 10.202.178.133 with SMTP id b127mr1948177oif.261.1508079254978; Sun, 15 Oct 2017 07:54:14 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Sun, 15 Oct 2017 07:53:54 -0700 (PDT) In-Reply-To: <20171015135740.GA7845@mathematik.tu-darmstadt.de> 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> From: Michael Shulman Date: Sun, 15 Oct 2017 07:53:54 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality To: Thomas Streicher Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" 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.