Yet another cubical type theory, but via a semantic approach

TL;DR

This paper introduces a new cubical type theory called naive cubical type theory and explores its semantics using the universe category framework, demonstrating its interpretability in various mathematical settings.

Contribution

It presents a novel semantic approach to cubical type theory, broadening its interpretability across different categorical models.

Findings

Admits interpretation in simplicial sets

Supports interpretation in cartesian cubical sets

Uses universe category framework for semantics

Abstract

We propose a new cubical type theory, termed (self-deprecatingly) the naive cubical type theory, and study its semantics using the universe category framework, which is similar to Uemura's categories with representable morphisms. In particular, we show that this new type theory admits an interpretation in a wide variety of settings, including simplicial sets and cartesian cubical sets.