From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.82.71 with SMTP id g68mr5951489vkb.119.1515424297881; Mon, 08 Jan 2018 07:11:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.31.165.19 with SMTP id o19ls63301vke.15.gmail; Mon, 08 Jan 2018 07:11:36 -0800 (PST) X-Received: by 10.176.77.109 with SMTP id k45mr2222035uag.37.1515424296838; Mon, 08 Jan 2018 07:11:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1515424296; cv=none; d=google.com; s=arc-20160816; b=UOWuB/Hcehma0doguNZAQtiyovKLRQQ3nLD7yNbiTSpoSq0YvLljOo55qILma1T3CA jicDOXcHe3J//6Gl701+WnnipQMseG2sWdkWtSDE0dwK8CqrkcilWpgOOrwlNGqtpk+m 33tKNUck7mT4J6WQa5QvSoEp2tShuTyugl9ha6gTUN6Il7mA0mJK87eGBNxRprfg2pWW 2do+kJXkyCU+GCHpFsaRDc7537Ky0eBjcWN8rXW2t7almzLj6hCPTyQZ9AhgKjd1Yt40 GHH7YEEzOfWi1Z8yTM5Q5GLcGcunohPtB9ONjMgLrTlUwK+3ZtsCJswpwnmq4sZjjMNU ITJg== 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=CTNNGiQnw1rVpSygyODJfpy0H2pkEO8vurVMWfSmK/M=; b=Pml7c3/LW5Z+MjdeeelEhW7GA9BdyjlwdO627XDfImG9SxwQTytNjSBkznHac4Yx3G DqqyApRHKnAeIdivcB9a+ph186ui/hMJlvTrvc77H4Ugv4YrzTXPxsrtNxB/bV3L9Dit FKe6iQKL4sZr5Q5GpDnmOpiMc8D3WKTQmqNjrECuYUP3RV5Tk0LQKjPD46uXLU6OX0al bJYDHZoIhZ8fThfTbSVwc3WmYwSOYaFxDzsjkVzEm/5pS+xjTw8yQNW/sIruNxhzHQnp wbC+vSBmwXIwttg6hR0QGDGtrYIEMa3gUzV7XqLMBDmDymNUSZa06cN6nDIoUEtLl4X6 Kh3g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=P2HXEVNK; spf=pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c05::234 as permitted sender) smtp.mailfrom=evanc...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yw0-x234.google.com (mail-yw0-x234.google.com. [2607:f8b0:4002:c05::234]) by gmr-mx.google.com with ESMTPS id g26si97836uak.3.2018.01.08.07.11.36 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 08 Jan 2018 07:11:36 -0800 (PST) Received-SPF: pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c05::234 as permitted sender) client-ip=2607:f8b0:4002:c05::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=P2HXEVNK; spf=pass (google.com: domain of evanc...@gmail.com designates 2607:f8b0:4002:c05::234 as permitted sender) smtp.mailfrom=evanc...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-yw0-x234.google.com with SMTP id r205so4399022ywb.3 for ; Mon, 08 Jan 2018 07:11:36 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=CTNNGiQnw1rVpSygyODJfpy0H2pkEO8vurVMWfSmK/M=; b=P2HXEVNKD3GflKfAAwoTXtYPwekOBRheh4Jk5X+gsidZagx3Vo8L9GIjdjApGam/2Y Ax+zYeJW7m0lZkD8MKofMGsOs5myuYCOfpQyatqXSnq5CdcB5dHppPwWf23uQ0Qhj2Wi F62W5sXuY1kx9RuZZvKsJzJulIUccS4R65Zefu7NNLg4pEY9lFol6UpI3v+d/I3WhCrT ke22K0xCOuwTrQ3qBD5gPizljq7I/adeZO5SRbmFoD9LyFQAAt4q5e9ctYXmycxyzhPr 0SKsrt1AWhneYw5jWK1X2Rx4wvpyEpWSFW/GBWVbxllO4waXAJuhDt0gObwYc9dXiy05 1pSw== X-Gm-Message-State: AKGB3mKRi+U7zRpS56uiLZAUr/i/BhC/QfMJKwtAZKHLxERs1LZwhhhn iJR53loAe6v7+2f/6J2t1G9UIsoKIMjBxtXxSvH8sw== X-Received: by 10.129.78.82 with SMTP id c79mr11257328ywb.509.1515424296178; Mon, 08 Jan 2018 07:11:36 -0800 (PST) MIME-Version: 1.0 Received: by 10.37.129.77 with HTTP; Mon, 8 Jan 2018 07:11:35 -0800 (PST) From: Evan Cavallo Date: Mon, 8 Jan 2018 10:11:35 -0500 Message-ID: Subject: computational higher type theory iv To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c07e0bcdba9bd05624536e0" --94eb2c07e0bcdba9bd05624536e0 Content-Type: text/plain; charset="UTF-8" Hello everyone, Part IV of our series on computational higher type theory is now available on the arXiv. This paper extends the type theory with a general class of higher inductive types and a homotopy fiber type. Our class of higher inductives includes all truncations, W-quotients, and localizations. Using the homotopy fiber type, we define an identity type (with an exact reduction rule for J on refl) as the family of fibers of the diagonal in the standard way, thereby giving a novel construction of an identity type in a cubical type theory. We inherit a canonicity result, that all closed terms of boolean type evaluate either to true or to false, from Part III. (In the methodology of computational type theory, it is not possible to disturb this result simply by adding new types. Rather, our contribution is to show that it is possible to define types satisfying expected rules for higher inductives.) We can also say that any closed 0-cell in a higher inductive type evaluates to an introduction form. Taken together, Parts I-IV define a cubical type theory capable of interpreting the univalence axiom, many higher inductive types, and identity types. We have therefore given a computational model for the bulk of the formal type theory defined in the HoTT book (excluding general indexed inductive and inductive-inductive types). arXiv paper: https://arxiv.org/abs/1801.01568 Evan Cavallo Robert Harper --94eb2c07e0bcdba9bd05624536e0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello everyone,

Part IV o= f our series on computational higher type theory is now available on the ar= Xiv. This paper extends the type theory with a general class of higher indu= ctive types and a homotopy fiber type. Our class of higher inductives inclu= des all truncations, W-quotients, and localizations. Using the homotopy fib= er type, we define an identity type (with an exact reduction rule for J on = refl) as the family of fibers of the diagonal in the standard way, thereby = giving a novel construction of an identity type in a cubical type theory.

We inherit a canonicity result, that all closed ter= ms of boolean type evaluate either to true or to false, from Part III. (In = the methodology of computational type theory, it is not possible to disturb= this result simply by adding new types. Rather, our contribution is to sho= w that it is possible to define types satisfying expected rules for higher = inductives.) We can also say that any closed 0-cell in a higher inductive t= ype evaluates to an introduction form.

Taken toget= her, Parts I-IV define a cubical type theory capable of interpreting the un= ivalence axiom, many higher inductive types, and identity types. We have th= erefore given a computational model for the bulk of the formal type theory = defined in the HoTT book (excluding general indexed inductive and inductive= -inductive types).

Evan Cavallo
Robert Harper
--94eb2c07e0bcdba9bd05624536e0--