Chris Kapulkin - Publications & Preprints
-
Homotopy limits in Coq, with Jeremy Avigad and Peter Lumsdaine
Submitted, 2013. [pdf] [Coq]
[arXiv]
Abstract: Working in Homotopy Type Theory, we provide a systematic study of basic homotopy limits and
related constructions. The entire development has been formally verified in the Coq interactive proof assistant.
-
Univalent categories and Rezk completion, with Benedikt Ahrens and Mike Shulman
Submitted, 2013. [pdf] [Coq]
[arXiv]
Abstract: We develop category theory within Univalent Foundations. We propose a definition of "category"
for which equality and equivalence of categories agree. Such categories satisfy a version of the Univalence Axiom, saying that the type of
isomorphisms between any two objects is equivalent to the identity type between these objects; we call them "saturated" or "univalent"
categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and
higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the
stack completion of a prestack.
-
The Simplicial Model of Univalent Foundations,
with Peter Lumsdaine and Vladimir Voevodsky
Preprint 2012. [pdf] [arXiv]
Abstract: We construct and investigate a model of the Univalent Foundations of Mathematics in the
category of simplicial sets.
To this end, we first give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then
construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in
several equivalent formulations, and show that it holds in our model.
-
Expressivness of positive coalgebraic logic, with Alexander Kurz and Jiri Velebil
In Advances in Modal Logic 2012. [pdf]
Abstract: Coalgebraic logic has been mostly developed for coalgebras over sets. This paper studies how
some well-known results (such as the one that the logic of all predicate liftings is expressive) transfer to coalgebras whose carriers are
posets.
-
Homotopy theoretic models of type theory, with Peter Arndt
In Springer LNCS 6690 (Typed Lambda Calculi and Applications 2011). [pdf]
[arXiv]
Abstract: 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 one can soundly interpret
dependent products and sums in it while also having a purely intensional
interpretation of the identity types.