17 citations · 30 across the 21 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2025
Yet another cubical type theory, but via a semantic approach
Chris Kapulkin, Yufeng Li
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…
cs.LO2025
(Pointed) Univalence in Universe Category Models of Type Theory
Chris Kapulkin, Yufeng Li
We provide a formulation of the univalence axiom in a universe category model of dependent type theory that is convenient to verify in homotopy-theoretic settings. We further devel…