Yet another cubical type theory, but via a semantic approach
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909971014221824 |
|---|---|
| author | Kapulkin, Chris Li, Yufeng |
| author_facet | Kapulkin, Chris Li, Yufeng |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_17548 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Yet another cubical type theory, but via a semantic approach Kapulkin, Chris Li, Yufeng Logic in Computer Science Category Theory Logic 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. |
| title | Yet another cubical type theory, but via a semantic approach |
| topic | Logic in Computer Science Category Theory Logic |
| url | https://arxiv.org/abs/2512.17548 |