From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.223.139.198 with SMTP id w6mr502049wra.4.1508056675921; Sun, 15 Oct 2017 01:37:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.197.15 with SMTP id v15ls919225wmf.2.canary-gmail; Sun, 15 Oct 2017 01:37:54 -0700 (PDT) X-Received: by 10.223.139.198 with SMTP id w6mr502047wra.4.1508056674903; Sun, 15 Oct 2017 01:37:54 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508056674; cv=none; d=google.com; s=arc-20160816; b=A3ZtBicQ07HxNw0EkxdRn/h5+37jV6phbq/VOAP6AslX+8MxTUIACfqJZABrF1UCCE NnrNcLODXnF+HwnZsSH0NBDgt1yUV5vl1ePZ1qLdZrpYKEIrvvF+W8PsOQwsyGeNnXrA ULnCHUizZtjDOBx7mvAiJvVP9+IC7tZyfAiv5bhzJrYckEmSxZXinVK7aJb16IJRgulT 33Pi+yV2g8+KTJRc/mZqdkiGH8KlsmWCmTSCfOhTHmCLog/zzNABGOKj33AtIw6C9PU7 6Ms1xW37RN9/ohi4gWdYp29bN/cyIr5W1pH7yhmqLxcq1lBD2quxAZm8L4ad4zUxGRv4 IpAw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from:arc-authentication-results; bh=Qt9qdXCznYypmyuuykNNYgWfPNlcnI6JXQw/Wcih+6U=; b=wPHX/G1xKWevEeAFCpR2lUXmLinLn2eRcNczHQvE+7eosCnf4mog5RjxstNHZWBdi7 aqkaoXzLNE9+ohMlUOTg2YrhHZWRBzlyVUlPP1TYe6WJ7eURoxuQxCVWfJEpJSpmwtQz NUKsziy/mdQ90GMn5Q9BwRiydsA2/8Kg110LxOWS7mNd2s6CWuPjCF+zZyE5DkKzaPQC b1Hjx+bcED/PcfAybqQE2cGDXhe3yfkiLsh2bS8+OmJR/mZlFZmxKsklyvVNOPNYBLKw 0uyO46L/x8kmvlU+Cx73xgOKZL+H32oLToCBbD0uv2hP29N1QgC+CV5fQRYHPNd5D21o qXdw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.134 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Return-Path: Received: from martell.ita.chalmers.se (martell.ita.chalmers.se. [129.16.226.134]) by gmr-mx.google.com with ESMTPS id p70si244017wma.1.2017.10.15.01.37.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Sun, 15 Oct 2017 01:37:54 -0700 (PDT) Received-SPF: neutral (google.com: 129.16.226.134 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) client-ip=129.16.226.134; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.134 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Received: from tyrell.ita.chalmers.se (129.16.226.132) by martell.ita.chalmers.se (129.16.226.134) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.845.34; Sun, 15 Oct 2017 10:37:54 +0200 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.0845.034; Sun, 15 Oct 2017 10:37:54 +0200 From: Thierry Coquand To: Thomas Streicher CC: Homotopy Type Theory Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Thread-Topic: [HoTT] A small observation on cumulativity and the failure of initiality Thread-Index: AQHTQ4nwR5ELY22PVUyO8hzaTeaYuqLgxlgAgAEG+gCAAAeDgIAAAbKAgAF5/QCAARoGAIAALsfi Date: Sun, 15 Oct 2017 08:37:54 +0000 Message-ID: <61005fc37ae1495bb2038467222db2e7@cse.gu.se> References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> ,<20171015074530.GA29437@mathematik.tu-darmstadt.de> In-Reply-To: <20171015074530.GA29437@mathematik.tu-darmstadt.de> Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_61005fc37ae1495bb2038467222db2e7cseguse_" MIME-Version: 1.0 --_000_61005fc37ae1495bb2038467222db2e7cseguse_ Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable 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 ab= straction is typed), and using set theoretic coding, one can use a global application op= eration (so that the interpretation is total). One can then checked by induction on= derivations that all judgements are valid for this interpretation. Thierry ________________________________ From: homotopyt...@googlegroups.com on beha= lf of Thomas Streicher Sent: Sunday, October 15, 2017 9:45:30 AM To: Gabriel Scherer Cc: Michael Shulman; Steve Awodey; Dimitris Tsementzis; Homotopy Type Theor= y Subject: Re: [HoTT] A small observation on cumulativity and the failure of = initiality 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 -- 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 e= mail to HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --_000_61005fc37ae1495bb2038467222db2e7cseguse_ Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable

 A quite detailed interpretation of type theory in set theory is pr= esented

in the paper of Peter Aczel "On Relating Type Theories and Set Theo= ries".

On can define directly the interpretation of lambda terms (pro= vided 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 th= is interpretation.


 Thierry

From: homotopyt...@google= groups.com <homotop...@googlegroups.com> on behalf of Thomas Streiche= r <str...@mathematik.tu-darmstadt.de>
Sent: Sunday, October 15, 2017 9:45:30 AM
To: Gabriel Scherer
Cc: Michael Shulman; Steve Awodey; Dimitris Tsementzis; Homotopy Typ= e Theory
Subject: Re: [HoTT] A small observation on cumulativity and the fail= ure of initiality
 
It is certainly tempting to assign meanings to der= ivations 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













--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsu...@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
 --_000_61005fc37ae1495bb2038467222db2e7cseguse_--