From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.37.97.196 with SMTP id v187mr321364ybb.87.1507570874487; Mon, 09 Oct 2017 10:41:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.225.140 with SMTP id k134ls182610ywe.31.gmail; Mon, 09 Oct 2017 10:41:13 -0700 (PDT) X-Received: by 10.37.9.66 with SMTP id u2mr323766ybm.83.1507570873694; Mon, 09 Oct 2017 10:41:13 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507570873; cv=none; d=google.com; s=arc-20160816; b=skahD2LmPwvDpgg+ee2erGvMQsYk72YznMXFbP+LfkEmfiiJfyI8M/HwnicxmMjUjr Yz5LEj0FRR9ZWjXdAptRrhWsRjYxHEU6K/HOBEB50h1z9IrYRom94VMS+J51XLkjJydL KPqNg2AVuerZOxKcaWDE03SuSlUPMo4BojMlQZGlafP4dfYn6VW/d/C8OdCvYlSozyaC v8136p6MltQznKsRsvoGVaam1mgO942gvZBiusPzkAh3EqmcFMCe+dpSvyVNH4s4+8Vh NoK6lVYAv1w4DZYJYu6qnV2fmU8oHw91qVkwyW8+Gb33lt2hjH8aYOlDjzzdtxjlr4VB wniA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:to:date:message-id:subject:content-transfer-encoding :from:arc-authentication-results; bh=lCvgRIiqHk+WyYiRbG7cklX3n02CmyqALz3ET5jszNk=; b=fdp8xYa98dE8LFNcah66oT+FY2R6mFPHObo1NP6DEXv6yS4gbD//uXimDI97tNPgVj egTtcweeG5o6OSp64BDAjeEUIiZ9YboYnRH18aBGfKqQbGNCMlnrcCV279mfB1a29Fpy yTVJ6rbhNq16AEeyE+xISNVabvVS44HdOmOoXcNEGcewY26MB1+LeQmNwz2PVFKpt4TL OQ7RJa9xq8BZ4g2/w/TlxuEp0R/MOd53xPotoRjhBake8fI0uUwaue/6sZcgjJI3jrfG k5A8Ea6yfHy5dRUKgA4bw3aMkDcGlbvs7CgDpMI6o/IcVj8f0TgmkXab/HiYZ0QEcHhh sXhQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.213 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Return-Path: Received: from Princeton.EDU (ppa01.Princeton.EDU. [128.112.128.213]) by gmr-mx.google.com with ESMTPS id r130si160521ywh.26.2017.10.09.10.41.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 09 Oct 2017 10:41:13 -0700 (PDT) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.213 as permitted sender) client-ip=128.112.128.213; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.213 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp202l.Princeton.EDU (csgsmtp202l.Princeton.EDU [140.180.223.155]) by ppa01.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id v99HfDxH009564 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Mon, 9 Oct 2017 13:41:13 -0400 Received: from nwk-93-248.nwk.ruw.rutgers.edu (pool-165-230-224-31.nat.rutgers.edu [165.230.224.31]) (authenticated authid=dtsement bits=0) by csgsmtp202l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id v99HfCeT025308 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Mon, 9 Oct 2017 13:41:13 -0400 From: Dimitris Tsementzis Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: A question regarding certain rules Message-Id: <01C857D9-9B30-4836-8F22-761A678B5D53@princeton.edu> Date: Mon, 9 Oct 2017 13:41:51 -0400 To: Homotopy Type Theory Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-10-09_04:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1707230000 definitions=main-1710090258 Dear all, Is there a type theory that has been considered in the literature which inc= ludes *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 exp= ression that must appear in p(t), and T is a type expression that may or ma= y not appear in C(T). An example of (R1) is (U-CUMUL) as in the HoTT book, i.e. cumulativity of u= niverses. An example of (R2) is (Nat-intro-2) as in the HoTT book, i.e. the successor= for Nat (with C(T) =3D=3D Nat). Best, Dimitris