Computational Higher Type Theory III: Univalent Universes and Exact Equality

TL;DR

This paper extends Cartesian cubical higher type theory to include univalent universes and exact equality, providing a computational interpretation with a deterministic operational semantics.

Contribution

It introduces a cumulative hierarchy of univalent Kan universes and exact equality within the cubical realizability framework, advancing the computational understanding of higher type theory.

Findings

Closed boolean terms evaluate to true or false

Establishes a computational interpretation of cubical higher type theory

Provides a deterministic operational semantics for cubical programs

Abstract

This is the third in a series of papers extending Martin-L\"of's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend this framework to include a cumulative hierarchy of univalent Kan universes of Kan types, exact equality and other pretypes lacking Kan structure, and a cumulative hierarchy of pretype universes. As in Parts I and II, the main result is a canonicity theorem stating that closed terms of boolean type evaluate to either true or false. This establishes the computational interpretation of Cartesian cubical higher type theory based on cubical programs equipped with a deterministic operational semantics.