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.

翻译：我们提出了一种新的立方类型理论，自嘲式地称之为朴素立方类型理论，并利用宇宙范畴框架（类似于上村的可表态射范畴）研究其语义学。特别地，我们证明了这种新型类型理论可在多种数学结构中实现解释，包括单纯集与笛卡尔立方集。