From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.80.244.1 with SMTP id r1mr2328944edm.3.1508148078753; Mon, 16 Oct 2017 03:01:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.80.219.194 with SMTP id s2ls5634249edk.5.gmail; Mon, 16 Oct 2017 03:01:18 -0700 (PDT) X-Received: by 10.80.204.74 with SMTP id n10mr2316552edi.2.1508148078003; Mon, 16 Oct 2017 03:01:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508148077; cv=none; d=google.com; s=arc-20160816; b=q5oIwF5kuJ9Voz7ZUT9LMXVinheckdgx2LgdC3un9B3yaVgNaCteKwQxGrRVMbySo3 4bkRfKL5pNmvzOqgngIHZui8mrrl79odK6RyhpGb2ZBhA1juWzPGnKj33gyYZZOj/yM7 ke/075A/FORgwZ80hRwK0w0Vose+SjpVQftcviK/5bUO9+xr09DAfAD0wm+8M8wDsfeD z28GQ1flPHXiFLtJE6m7TJHD8dWF1C7QaG76hb1Q3OUedi4jR+nN3KQezHYKZ0oXrtZK 9nW9I0lQsnYDVZ7kJrgg6T/Ei/YHnMTzi5r1ovfysicnvY/TJ39aRu6C8/C/EQrF79E+ rjRg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:arc-authentication-results; bh=BuOdDs4ZHd4wpFupcd+yaCCvaJPDcSmNhN/XwRFa0I0=; b=vU5r5NwMi6MUdmbAMS8S/f8NWGxxcGsqU9K28rD2I1E253O9Sceg8RBzBf+uGNbg+K RfJK9HDC3Y54fLvZmIsIRL/OJR0+k4lu3vexKIhd3vM4AqetoO3huAKdx2+vuQHGKxJt umeAV96lYYMNeWnRKESOFPJnFOx71g860nC55q7mEd5sYAPn7/cxFJdnoRqsMJBVdawA uJG0yzxeTISFl0Qw/1CeVnAT+NzDtaEDDcexdksNaw4OdWxXb0aa4PMxUj/rkbPLU4yV QFLD0f7PuD1l60WkMavzLCV5W9WPBQUemY/n+GdwyAH462OqWMaJe7Y92xLTSVDdwwgn S2Iw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx500.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.156.225]) by gmr-mx.google.com with ESMTPS id w24si329870edl.5.2017.10.16.03.01.17 for (version=TLS1 cipher=AES128-SHA bits=128/128); Mon, 16 Oct 2017 03:01:17 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) client-ip=130.83.156.225; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.225 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) by lnx500.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v9G9vni5028972; Mon, 16 Oct 2017 11:57:51 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id v9GA18RF021795; Mon, 16 Oct 2017 12:01:08 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id B275A1A4679; Mon, 16 Oct 2017 12:01:08 +0200 (CEST) Date: Mon, 16 Oct 2017 12:01:08 +0200 From: Thomas Streicher To: Michael Shulman Cc: Homotopy Type Theory Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Message-ID: <20171016100108.GB4118@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> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.10.16.95416 X-PMX-RELAY: outgoing > 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". You can assign meaning to derivations AND define a partial interpretation function for prejudgements and then show by single induction on derivations that the meaning assigned to a derivation coincides with the meaning assigned to the judgement it derives. So things can be reconciled though assigning meaning to derivations is a bit of overkill... Thomas