From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.6.16 with SMTP id 16mr17746831iog.105.1512525290981; Tue, 05 Dec 2017 17:54:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.69.143 with SMTP id c15ls480493itd.9.canary-gmail; Tue, 05 Dec 2017 17:54:49 -0800 (PST) X-Received: by 10.107.164.225 with SMTP id d94mr17356809ioj.12.1512525289835; Tue, 05 Dec 2017 17:54:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1512525289; cv=none; d=google.com; s=arc-20160816; b=OOuCITwoN/Z8CXJG9Rv5QbUQpIZvtoIQxPbuBldRgAJ6NKh5DfZBz3oreI6KenT6W2 b4AVSJhF8GN7ObOVRqApgvrBN8y24T5iMzIPg/PhyAY1FjJn2BexwXAp0ppIsLZm+33w WB8b/pEobXpS/xDHNkKNxAq/CcbcCviKajQP4qAS+1GufFRAonuL6VOijsoPfUp0M9ij z756arEtHfdMEyCaXSVmXrEMnHNWlbrTSboBB0131xhvRHK7KMhwPl44inQH3Z3ekcLx jximPfYfTvsVkgRfKxTVSgY20JUQjn29dSP5SDkSo/tIKOJjnGORCjCfT57zmAMSIoBc kGZw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=Wgw3DuQo9uQntVx4+wpOI19/KbXFWxpTAmxB3+BwzDY=; b=jZI5Ne0FlMz4gc2oKqeyql94rOg7N5rmhJ1KenLa/IwpW5xkajHhPKHEMcQnm05h8G IMZ1eqxVYjZMtTcGmmAO2hEaT3RT/buB+DTUahkY2Oe1S1PnBUqcGhBFKtq1Gd74Tw0x D3i1qsU4bj0mxaeYCtS3CyQpYmkWvw7Wa5mUsyIRJZAp7DJYM5jj1hhgMmEWTF1zG4z1 /DgBgpRDBPobsFGDbgUMB8b33kdwerV5df0TpAORaVxwMbw6+YEn9dUpZmCQgFyEvDKD FJktLO0EnXOp9k5qarbN3WCRIJQbQ5HvNrL63AmUHRcfVwCpHHdt3Fh9aFEVDbI/KGzo vEkA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cs-cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=Gj0TBGcp; spf=neutral (google.com: 2607:f8b0:400c:c08::230 is neither permitted nor denied by best guess record for domain of r...@andrew.cmu.edu) smtp.mailfrom=r...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-ua0-x230.google.com (mail-ua0-x230.google.com. [2607:f8b0:400c:c08::230]) by gmr-mx.google.com with ESMTPS id k4si97095ioc.4.2017.12.05.17.54.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Dec 2017 17:54:49 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:400c:c08::230 is neither permitted nor denied by best guess record for domain of r...@andrew.cmu.edu) client-ip=2607:f8b0:400c:c08::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cs-cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=Gj0TBGcp; spf=neutral (google.com: 2607:f8b0:400c:c08::230 is neither permitted nor denied by best guess record for domain of r...@andrew.cmu.edu) smtp.mailfrom=r...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-ua0-x230.google.com with SMTP id v20so1793604uaj.0 for ; Tue, 05 Dec 2017 17:54:49 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs-cmu-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:from:date:message-id:subject:to; bh=Wgw3DuQo9uQntVx4+wpOI19/KbXFWxpTAmxB3+BwzDY=; b=Gj0TBGcpA6L7t8JUMrH8hctJiGXplbqZjK88FUU/jUNZIpsJnOomWVwbsY76VJ3tFr TB1pcwmxZsVFXsa2YZ5Ir4u0kSd1O0QsqpMq8Ozcclo+7+INBndo7PDLdflUWYmCMHYl bXNy6RJT2fVxKNtxeiE7qLX2bXx6kgJBphQDUwJpGS1AsPGbsow+fU01d4Brtjf+n8u+ Ktfq1EwwCrCzaPyHGgHL8WFTA3vGsdfiKhA5U2dhO07oB/bxz0Aj19vGF3cjAZnCPSx/ E/sL6W7VSf6QmmJXligr36sYQ8JMFOW6acc6Wt/NBd65Mh+7k2htj06XsWofjBnFtdCR g2LA== X-Gm-Message-State: AKGB3mLJDpiuKZkPiaMFNWH8ORBpHy0xbnRK7Wq4rT5hMw5PbTyDxosU PwaERGPepp7RRfje8b+B4qAW7ZQfO8UQnXJ4N3/8aQ== X-Received: by 10.159.35.234 with SMTP id 97mr8072227uao.119.1512525288985; Tue, 05 Dec 2017 17:54:48 -0800 (PST) MIME-Version: 1.0 From: "Prof. Robert Harper" Date: Wed, 06 Dec 2017 01:54:38 +0000 Message-ID: Subject: computational higher type theory iii and cartesian cubical formal type theory To: "homotopyt...@googlegroups.com" Content-Type: multipart/alternative; boundary="94eb2c03caf0906de8055fa23cb7" --94eb2c03caf0906de8055fa23cb7 Content-Type: text/plain; charset="UTF-8" This is to announce progress on a programming language, proof theory, and model for univalent type theory based on the Cartesian cube category. First, Part III of our three-part series "Computational Higher Type Theory" provides a full development of univalent Cartesian cubical type theory in the computational setting. In contrast to formal type theories, the computational approach begins with the notion of program, which is used to provide a mathematical meaning explanation (computational semantics) of cubical type theory. We develop a two-level type system (in the general style of Voevodsky's HTS) that includes an exact extensional equality judgment for types and elements; a cumulative hierarchy of univalent Kan universes of Kan types; an internalization of exact equality and other pretypes lacking Kan structure; and a cumulative hierarchy of pretype universes. A key technical contribution is a generalization of the Kan condition to admit diagonal "tubes", which is needed to account for univalent universes in the Cartesian setting. The main result is a canonicity theorem stating that closed programs of Boolean type evaluate to either true or false. The full type theory is implemented in the open-source RedPRL proof assistant, which is freely available for download and experiment. Part IV of the series, on higher inductive types, is expected to be released shortly. arXiv paper: https://arxiv.org/abs/1712.01800 RedPRL: http://redprl.org/ A draft of a second paper, joint work with Brunerie, Coquand, and Licata, develops a formal Cartesian cubical type theory with univalent universes, and a constructive model in Cartesian cubical sets, based on the set of trivial cofibrations for the Cartesian cube category introduced by Coquand. Much of the model, including fibrancy of glue (equivalence extension) types, which is the key lemma for univalent and Kan universes, has been formalized in Agda using the internal language technique developed by Orton and Pitts. The formal type theory and internal language model are open-ended with respect to extensions of the allowed filling problems, and therefore provide a potential route to comparing with the Cohen, Coquand, Huber, and Moertberg model. paper link: https://github.com/dlicata335/cart-cube/blob/master/cart-cube.pdf formalization: https://github.com/dlicata335/cart-cube In our opinion, the line of work described in these two papers represents a successful application trinitarianism: ideas were introduced in a model, pushed forward in a proof theory, and completed in a programming language, in such a way that the advances apply in all three settings. Carlo Angiuli Kuen-Bang Hou (Favonia) Robert Harper -- (c) Robert Harper. All rights reserved. --94eb2c03caf0906de8055fa23cb7 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This is to announce progress on a programming la= nguage, proof
theory, and model for univalent type theory based o= n the Cartesian
cube category.

First, Pa= rt III of our three-part series "Computational Higher Type
T= heory" provides a full development of univalent Cartesian cubical
type theory in the computational setting. In contrast to formal type<= /div>
theories, the computational approach begins with the notion of
program, which is used to provide a mathematical meaning explanatio= n
(computational semantics) of cubical type theory.=C2=A0 We deve= lop a
two-level type system (in the general style of Voevodsky= 9;s HTS) that
includes an exact extensional equality judgment for= types and
elements; a cumulative hierarchy of univalent Kan univ= erses of Kan
types; an internalization of exact equality and othe= r pretypes lacking
Kan structure; and a cumulative hierarchy of p= retype universes.=C2=A0 A key
technical contribution is a general= ization of the Kan condition to
admit diagonal "tubes",= which is needed to account for univalent
universes in the Cartes= ian setting. The main result is a canonicity
theorem stating that= closed programs of Boolean type evaluate to
either true or false= . The full type theory is implemented in the
open-source RedPRL p= roof assistant, which is freely available
for download and experi= ment.

Part IV of the series, on higher inductive t= ypes, is expected=C2=A0
to be released shortly.


A draft of a second paper= , joint work with Brunerie, Coquand, and
Licata, develops a forma= l Cartesian cubical type theory with univalent
universes, and a c= onstructive model in Cartesian cubical sets, based
on the set of = trivial cofibrations for the Cartesian cube category
introduced b= y Coquand.=C2=A0 Much of the model, including fibrancy of glue
(e= quivalence extension) types, which is the key lemma for univalent
and Kan universes, has been formalized in Agda using the internal
language technique developed by Orton and Pitts.=C2=A0 The formal type
theory and internal language model are open-ended with respect to
extensions of the allowed filling problems, and therefore provide = a
potential route to comparing with the Cohen, Coquand, Huber, an= d
Moertberg model.

formalization: https:/= /github.com/dlicata335/cart-cube

In our opinio= n, the line of work described in these two papers
represents a su= ccessful application trinitarianism: ideas were introduced in a
m= odel, pushed forward in a proof theory, and completed in a
progra= mming language, in such a way that the advances apply in all
thre= e settings.

Carlo Angiuli
Kuen-Bang Hou = (Favonia)
Robert Harper

--
(c) Robert Harper. All rights reserved.
--94eb2c03caf0906de8055fa23cb7--