From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.175.73 with SMTP id x9mr1738575ywj.87.1507604778000; Mon, 09 Oct 2017 20:06:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.129.45.133 with SMTP id t127ls485162ywt.42.gmail; Mon, 09 Oct 2017 20:06:17 -0700 (PDT) X-Received: by 10.129.48.201 with SMTP id w192mr1814156yww.22.1507604777284; Mon, 09 Oct 2017 20:06:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507604777; cv=none; d=google.com; s=arc-20160816; b=qS4gsJrrO5uqBRzI0pmzAh8f4H8VBsHXCq3f4Byr+e89SfA+LsvZtl6xixB3mekQvp 6nCeZPqj0KxLJGhvP0Q4Jr5k/zBluMrsbf1uv4cZxPiaEeQ/WtslEtU/N1QKpWj+Z2d5 1Fz279SF0J3x+dYDjRDeHh72MBJsXcp/1PfpYB2ayMtVrt2Vc68QFXbiMZKxsVUunEmS BIcCxk+oEIXxiGt9Ulm7QdeB8St3gkAl8wt7OP80KGAb3bbrrC2Avyq7w7Z7TQn6Ylbs r2I2GODpyo/3SSfDfl9zWnnL5d7oNd0TwsBhHsB+0WA2WTcnPyBFPI+7b4CvsH8tNtT4 99IQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:arc-authentication-results; bh=+S82AIyFLTNzZRvrueQ4kEHFM5Z+ZUcD/WtxtXpUaQA=; b=bYko/zF14h9vPKTuzlaPi+e2NWnhlwuzbABs4XxWswyHz7kllUH/ohdkL8ymO+eW1G kdjj0nLJY/9uMO4+RvP7OypidkAZJexk6Hm3kXcGGnsyIaPYMueFkEjfQex0hNcX5zTZ jl1DbbR8fBbiWEAQp3sePJNCuIJqfNkVxQgd/ODfMfIM/iLmTaOBOF9xg6zVMptp72XJ q6zIWAgzkdWx5efeAmbVHatXMerog/BH0NGOW+Ev7XIWf9iOwu1SsW1JMNjSG50eKnV3 f28Gs/AOOoVCgyqEZW8j+RN8IChmdeThj1ABNLjzExNhgVCuMoF1RkbEfiFMPEgea9rR CkIQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Return-Path: Received: from Princeton.EDU (ppa03.Princeton.EDU. [128.112.128.214]) by gmr-mx.google.com with ESMTPS id r130si213704ywh.26.2017.10.09.20.06.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 09 Oct 2017 20:06:17 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) client-ip=128.112.128.214; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.214 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp203l.Princeton.EDU (csgsmtp203l.Princeton.EDU [140.180.223.156]) by ppa03.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id v9A36GWn001573 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Mon, 9 Oct 2017 23:06:16 -0400 Received: from mac-e0accb9c0fda.home (pool-96-239-82-13.nycmny.east.verizon.net [96.239.82.13]) (authenticated authid=dtsement bits=0) by csgsmtp203l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id v9A36Fmg026760 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Mon, 9 Oct 2017 23:06:16 -0400 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] A question regarding certain rules From: Dimitris Tsementzis In-Reply-To: <0d00219f-470f-cd84-98de-5eff1c2a4ea4@skyskimmer.net> Date: Mon, 9 Oct 2017 23:06:53 -0400 Cc: Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: References: <01C857D9-9B30-4836-8F22-761A678B5D53@princeton.edu> <0d00219f-470f-cd84-98de-5eff1c2a4ea4@skyskimmer.net> To: =?utf-8?Q?Ga=C3=ABtan_Gilbert?= X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-10-09_07:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=8 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1707230000 definitions=main-1710100044 Thanks. Yes, this is of course entirely compatible with my description, yet= I am not sure it captures what I was after.=20 I will have to think more about whether your example suffices for my purpos= es. Dimitris > On Oct 9, 2017, at 13:54, Ga=C3=ABtan Gilbert = wrote: >=20 > Does T:=3DType0, C(T):=3DType1, t:=3Dnat and p(t):=3Dnat->nat count? If s= o HoTT has this. If not why not? >=20 > Ga=C3=ABtan Gilbert >=20 > On 2017-10-09 19:41, Dimitris Tsementzis wrote: >> Dear all, >> Is there a type theory that has been considered in the literature which = includes *both* the following rules >> =CE=93 |- t : T >> =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= (R1) >> =CE=93 |- t : C(T) >> =CE=93 |- t : T >> =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= (R2) >> =CE=93 |- p(t) : C(T) >> where C(T) is a type expression, p(t) is a term expression, t is a term = expression that must appear in p(t), and T is a type expression that may or= may not appear in C(T). >> An example of (R1) is (U-CUMUL) as in the HoTT book, i.e. cumulativity o= f universes. >> An example of (R2) is (Nat-intro-2) as in the HoTT book, i.e. the succes= sor for Nat (with C(T) =3D=3D Nat). >> Best, >> Dimitris >=20 > --=20 > 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= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.