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