From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.168.76 with SMTP id r73mr175072lfe.41.1508053535761; Sun, 15 Oct 2017 00:45:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.46.11 with SMTP id u11ls1486609lju.13.gmail; Sun, 15 Oct 2017 00:45:34 -0700 (PDT) X-Received: by 10.46.57.19 with SMTP id g19mr196247lja.3.1508053534497; Sun, 15 Oct 2017 00:45:34 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508053534; cv=none; d=google.com; s=arc-20160816; b=A+qVNCxNGzn3X4DQoOIj3gcFtu+DON3EvqUIUVGmNSuxlZ9sxnTTiASd/qHoA4Ww5x f9g8jXZrdAftBQIL/VOuoHd3DTSOzxCFb9Zj3DbBd6rl1DFFHschhFX3ytTDTIJOk/g6 ea27ykAGNktjqFiOzsaamP/yyS6iKC9hS7fYHxhViDZEYQ110211oHSCi9sh4nI5vBgD YDHPEDXStD8l+J6AYTTADLZ2r4aVRqi3TlEwA+t1eTT0U7dJBs9vUelewCs2snK3lEjy eFJXMaK45ag8IzoAsNcaRNVe8zDI3FSAW//voS/nVIbpNHxQZF7QddCSNQgmB3O5ixGB pNNA== 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=IUd9+aMc/Qr7TA/vpuVnCM0DJbMdNKOi5G0+x9/YlME=; b=oTbnCSjHrSiZklzmcgl2XICJsnAwX/Z1B7KkCqFR+FUpnEjfOp9red0s834shPUipw WOijt29KAIDJMpGSYz9uBCH55awlvSM0AmkG9igJLYaZ77NpNFAqpuVLhyJQH6YvFLaI pt8GYrAqJM7uQBg44xOvcmfIEAvqkjmBTnuIDW78Md0VBYrmnG6J3ou5e3QMQlyFLgfR rAvHrqrsOihq/mHi6qIp95VN2sc5G2rbJ5TBgzrD+rfE8Xke+RJtnZzSaMAR+MoVOnpg 4Aa2c2qrByovSf2H5tBHPcXAYg0goi1Zp8zukxjS8D0D9J9M+5nAs/cmuv198kd8q8pZ bimA== 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 c185si179761lfd.5.2017.10.15.00.45.34 for (version=TLS1 cipher=AES128-SHA bits=128/128); Sun, 15 Oct 2017 00:45:34 -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 v9F7gCSC010836; Sun, 15 Oct 2017 09:42:13 +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 v9F7jURF007675; Sun, 15 Oct 2017 09:45:30 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 9AB291A0D1C; Sun, 15 Oct 2017 09:45:30 +0200 (CEST) Date: Sun, 15 Oct 2017 09:45:30 +0200 From: Thomas Streicher To: Gabriel Scherer Cc: Michael Shulman , Steve Awodey , Dimitris Tsementzis , Homotopy Type Theory Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Message-ID: <20171015074530.GA29437@mathematik.tu-darmstadt.de> References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> 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.15.73616 X-PMX-RELAY: outgoing It is certainly tempting to assign meanings to derivations and then to show that different derivations of the same judgement get assigned the same meaning. 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. Most people have gone this way at least when they took pains to write down the interpretation function at all. BTW the above allows one to show that assigning a meaning to derivations just depends on the judgement: one jyust has to show that the meaning assigned to a derivation of a judgement J coincides with the meaning assigned to J beforehand. Thomas