computational higher type theory iii and cartesian cubical formal type theory

computational higher type theory iii and cartesian cubical formal type theory

[Prof. Robert Harper]

[-- Attachment #1: Type: text/plain, Size: 2804 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 3698 bytes --]