72 citations · 212 across the 10 of their papers we have counts for
10 papers
Synthetic approach to the Quillen model structure on topological spaces
Sterling Ebel, Chris Kapulkin
We provide an axiomatic treatment of Quillen's construction of the model structure on topological spaces to make it applicable to a wider range of settings, including -generated…
Closed symmetric monoidal structures on the category of graphs
Chris Kapulkin, Nathan Kershaw
We show that the category of (reflexive) graphs and graph maps carries exactly two closed symmetric monoidal products: the box product and the categorical product.
Homotopical inverse diagrams in categories with attributes
Chris Kapulkin, Peter LeFanu Lumsdaine
We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes and an ordered homotopica…
The homotopy theory of type theories
Chris Kapulkin, Peter LeFanu Lumsdaine
We construct a left semi-model structure on the category of intensional type theories (precisely, on ). This presents an -category of su…
Locally Cartesian Closed Quasicategories from Type Theory
Chris Kapulkin
We prove that the quasicategories arising from models of Martin-Löf type theory via simplicial localization are locally cartesian closed.
Quasicategories of Frames of Cofibration Categories
Chris Kapulkin, Karol Szumiło
We show that the quasicategory of frames of a cofibration category, introduced by the second-named author, is equivalent to its simplicial localization.
Homotopy limits in type theory
Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges…
Univalent categories and the Rezk completion
Benedikt Ahrens, Chris Kapulkin, Michael Shulman
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this syst…
The Simplicial Model of Univalent Foundations (after Voevodsky)
Chris Kapulkin, Peter LeFanu Lumsdaine
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categori…
Homotopy Theoretic Models of Type Theory
Peter Arndt, Chris Kapulkin
We introduce the notion of a logical model category which is a Quillen model category satisfying some additional conditions. Those conditions provide enough expressive power that o…