From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.71.131 with SMTP id m3mr720482wmi.19.1508075862771; Sun, 15 Oct 2017 06:57:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.38.134 with SMTP id m128ls991186wmm.4.gmail; Sun, 15 Oct 2017 06:57:41 -0700 (PDT) X-Received: by 10.28.128.211 with SMTP id b202mr692829wmd.5.1508075861906; Sun, 15 Oct 2017 06:57:41 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508075861; cv=none; d=google.com; s=arc-20160816; b=fkTqXruacZ9U4YPqiCDcKlazMCapCssqixFEcMG1V4R+iL9FAlEiVI3c9kwlaLNhKC Wr4uzXp1s6d1oO1eLXP8YnxsSZMtPozq/eqfxR/Nm60+PaZsE7z7nSbdxohCBL672/IF 4ykxNtSSR/j2agrog47y8Vg8g2wnPqjj3nrC3UHSqQhMEUS20Rp0w9zvpBkGdlm7z7Qn ZeFYu5HliYsQYLfki6CB+TGzk1ICpQ58SoOyGrXGE4A96yLKTSafappJwLtibOxFjaQx DWM6X5iJ/y/BfvOuc4xWIepmzILQ9NF2UCuaL6SViS+DhyenUjGTdL0urfuJ+adWVWY4 kCtw== 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=TkC/BJA17TK8DqprYanCrNjPQ/0PiMpBl4Ybjra6Mgg=; b=TQZbpZr/zbqCZhAdgroeOv0YLpZ3rfm71ECZ5YR+Kp3Q2eKKtNdYaoOyu6nzk1D7jc leN5wwltIwcpBi2Ry4bdhEo6xoPUU1ES0GMcSmUT/MVV0nBQNkydoOdsWLNlK/6Vt1MO O4GrO85yakbK1O6keLcfNP5lZvlLhr5afJ/4bG1nWz9BbKJI6N/tfIKAi7kZdDxXnVJ/ IlOxrqdjgZPwnvuRiOv/8dm/v/oZYVZFUDiR8OMShagmFE+gVXYg94Mj7aQ88aQ7it5q 6VCpZobiJOS5HEeMpsnEydzC8nsFkajxJoKtDSYGx5cb8Qg1ct6kdASvlp3JYy9e2U0e RE1w== 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.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from lnx503.hrz.tu-darmstadt.de (mail-relay15.hrz.tu-darmstadt.de. [130.83.156.239]) by gmr-mx.google.com with ESMTPS id k37si175137wre.0.2017.10.15.06.57.41 for (version=TLS1 cipher=AES128-SHA bits=128/128); Sun, 15 Oct 2017 06:57:41 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239; 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.239 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 lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v9FDveSo019771; Sun, 15 Oct 2017 15:57:40 +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 v9FDveRF009876; Sun, 15 Oct 2017 15:57:40 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 4B0241A491D; Sun, 15 Oct 2017 15:57:40 +0200 (CEST) Date: Sun, 15 Oct 2017 15:57:40 +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: <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> 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.135116 X-PMX-RELAY: outgoing > > 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