From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.202.4 with SMTP id a4mr164851lfg.32.1508059582554; Sun, 15 Oct 2017 02:26:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.77.200 with SMTP id c69ls591428ljd.10.gmail; Sun, 15 Oct 2017 02:26:21 -0700 (PDT) X-Received: by 10.25.202.4 with SMTP id a4mr164850lfg.32.1508059581133; Sun, 15 Oct 2017 02:26:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508059581; cv=none; d=google.com; s=arc-20160816; b=A4/darECDpTcxrIpf2Z0/7EIFjC6CGHLSiHDQeozk311gzLmRVB3kxjxZroykagF0H 1DhQDcB3tEfvdbroJYbQAYGUFuwIh94EuxZfj/Dz65adB3kL9ozYNv7NJ0pKBnn5LyIy g6vunn2i2CmDoPEsoBRcefhbQdnkukZk12FZQn/0XFTSuuuAyjtWY3bUTVv1a9hGwq4o wt1bqghkUj4KZx+52oaV/JI+F/9jnx5T+Wc+NN8r6nQApnnoyrN1LtiA2GzuLB8aJrZi jPEl+7NunNep/J+wTHtZvCM0s7gPuee5u/D1j+6p/9eBBqFhC9h+HzJyO+dfpiyLSIuF f3Ew== 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=lXb1t8FJLJSkGnQ0g8sTqE8fVjY0f/0iEEKMOk+lpOU=; b=cl4yBwLk8WWa8TnbXrJpiluDaWSqpDlVhr1R6hGVYmiZSCqRjLXRgSDyl5N+h2FG2r bESjAUSOGJbuBPk0h65zjm33En/iEQdG1ZZ5Z2kYEYZc+kQFCKpzSJtfW6ObdFUDR3tV eUtt2s0DPGUrggUhZS5xpbhpvRGHCqxcHc8fIf8Otn0dd+bP46makqqLwEaQIUXdYO// UyT0Ib5WKWWHnsFFzEbW9hXT/0lRfc/qGm+wRQHsGvxHaMl6ic3VTfroq6XohzyhhVVM i4Scn4Kpj2NisDwEPNtCTtlhScUDmpQSq3KaT0TwSg6W1uQ6LXW4l2fy32iPJuw2E8H9 Vxpg== 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 w14si242807lfk.2.2017.10.15.02.26.20 for (version=TLS1 cipher=AES128-SHA bits=128/128); Sun, 15 Oct 2017 02:26:20 -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 v9F9MxSv008291; Sun, 15 Oct 2017 11:22:59 +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 v9F9QHRF008200; Sun, 15 Oct 2017 11:26:17 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 4C6D91A0D1C; Sun, 15 Oct 2017 11:26:17 +0200 (CEST) Date: Sun, 15 Oct 2017 11:26:17 +0200 From: Thomas Streicher To: Thierry Coquand Cc: Homotopy Type Theory Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Message-ID: <20171015092617.GA684@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> <61005fc37ae1495bb2038467222db2e7@cse.gu.se> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <61005fc37ae1495bb2038467222db2e7@cse.gu.se> 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.91816 X-PMX-RELAY: outgoing > A quite detailed interpretation of type theory in set theory is presented > > in the paper of Peter Aczel "On Relating Type Theories and Set Theories". > > On can define directly the interpretation of lambda terms (provided that abstraction is > > typed), and using set theoretic coding, one can use a global application operation > > (so that the interpretation is total). One can then checked by induction on derivations > > that all judgements are valid for this interpretation. Thanks, Thierry, for pointing this out. But Peter's method does not extend to arbitrary split models of dependent type theory. What Peter uses here intrinsically is that everything is a set since otherwise he couldn't interpret type theoretic quantification. My interpretation got partial on pseudoexpressions since pseudoterms can't be understood as pseudo-type-expressions. I don't see how Peter's method extends to interpretation of realizability or (pre)sheaf models of dependent type theories not to speak of arbitrary contextual cats or other split categorical models of dependent type theories. Thomas