Yet another cubical type theory, but via a semantic approach
Logic in Computer Science
2025-12-22 v1 Category Theory
Logic
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.
Keywords
Cite
@article{arxiv.2512.17548,
title = {Yet another cubical type theory, but via a semantic approach},
author = {Chris Kapulkin and Yufeng Li},
journal= {arXiv preprint arXiv:2512.17548},
year = {2025}
}
Comments
78 pages; comments welcome