6 papers
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…
Extensional concepts in intensional type theory, revisited
Chris Kapulkin, Yufeng Li
Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional…
(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…
A Toolkit for Structured Lifts
Chris Kapulkin, Yufeng Li
We develop a general framework for working with structured lifting problems, establishing closure and uniqueness properties of their solutions. In a subsequent paper, we apply thes…
Pushforwards in Inverse Homotopical Diagrams
Chris Kapulkin, Yufeng Li
We establish a sufficient condition for the category of homotopical inverse diagrams to be closed under pushforward inside the category of inverse diagrams in a fibration category.
Logical Structure on Inverse Functor Categories
Marcelo Fiore, Chris Kapulkin, Yufeng Li
Inspired by recent work on the categorical semantics of dependent type theories, we investigate the following question: When is logical structure (crucially, dependent-product and…