17 citations · 30 across the 21 of their papers we have counts for
21 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…
(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…
Biclosed monoidal structures on the categories of digraphs and graphs
Adrien Grenier, Chris Kapulkin
We show that the categories of directed and undirected reflexive graphs carry exactly two (up to isomorphism) biclosed monoidal structures.
Cubical models of -presheaves and the Bousfield-Kan formula
Kensuke Arakawa, Daniel Carranza, Chris Kapulkin
We construct the covariant and the cocartesian model structures on the slice categories of cubical sets and marked cubical sets, respectively. As an application, we derive a versio…
Derived mapping spaces of -categories
Kensuke Arakawa, Daniel Carranza, Chris Kapulkin
We prove the Derived Mapping Space Lemma, which generalizes the central theorem of Cisinski's work on calculus of fractions for -categories, and allows us to provide a unif…
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.
Topological data analysis using persistent discrete homology
Chris Kapulkin, Nathan Kershaw
We propose persistent discrete homology as a tool for topological data analysis and discuss its advantages over the existing methods. In particular, we provide empirical evidence t…
Categorical foundations of discrete dynamical systems
Daniel Carranza, Chris Kapulkin, Nathan Kershaw +2
We develop categorical foundations of discrete dynamical systems, aimed at understanding how the structure of the system affects its dynamics. We introduce the notion of cycle sets…
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…
Faster computations of discrete homology
Chris Kapulkin, Nathan Kershaw
Machine computation of the discrete homology of graphs has stopped at degree two. We present an algorithm that reaches degree four. It generates the singular cubes inductively, pai…
Homotopy -types of cubical sets and graphs
Chris Kapulkin, Udit Mavinkurve
We give a new construction of the model structure on the category of simplicial sets for homotopy -types, originally due to Elvira-Donazar and Hernandez-Paricio, using a right t…
Calculus of Fractions for Quasicategories
Daniel Carranza, Chris Kapulkin, Zachery Lindsey
We describe a generalization of Gabriel and Zisman's Calculus of Fractions to quasicategories, showing that the two essentially coincide for the nerve of a category. We then prove…
Diagonal Lemma for Presheaves on Eilenberg-Zilber Categories
Daniel Carranza, Chris Kapulkin, Liang Ze Wong
The diagonal lemma asserts that if a map of bisimplicial sets is a levelwise weak equivalence in the Kan-Quillen model structure, then it induces a weak equivalence of the diagonal…
Cofibration category of digraphs for path homology
Daniel Carranza, Brandon Doherty, Chris Kapulkin +3
We prove that the category of directed graphs and graph maps carries a cofibration category structure in which the weak equivalences are the graph maps inducing isomorphisms on pat…
2-adjoint equivalences in homotopy type theory
Daniel Carranza, Jonathan Chang, Chris Kapulkin +1
We introduce the notion of (half) 2-adjoint equivalences in Homotopy Type Theory and prove their expected properties. We formalized these results in the Lean Theorem Prover.
The law of excluded middle in the simplicial model of type theory
Chris Kapulkin, Peter LeFanu Lumsdaine
We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence.
Cubical models of -categories
Brandon Doherty, Chris Kapulkin, Zachery Lindsey +1
We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting…
A co-reflection of cubical sets into simplicial sets with applications to model structures
Chris Kapulkin, Zachery Lindsey, Liang Ze Wong
We show that the category of simplicial sets is a co-reflective subcategory of the category of cubical sets with connections, with the inclusion given by a version of the straighte…
Internal Languages of Finitely Complete -categories
Chris Kapulkin, Karol Szumiło
We prove that the homotopy theory of Joyal's tribes is equivalent to that of fibration categories. As a consequence, we deduce a variant of the conjecture asserting that Martin-Löf…
Univalence in Simplicial Sets
Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky
We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.