Chris Kapulkin  Publications & Preprints

Homotopy type theory, as part of the Univalent Foundations Project
Book, 2013. [web]
About: The book is intended as a first systematic exposition of the basics of univalent foundations, and a
collection of examples of this new style of reasoningbut without requiring the reader to know or learn any formal logic, or to use any
computer proof assistant.

Homotopy limits in type theory, 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
Accepted for publication, 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
highercategorical 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 vol. 9, 2012, pp. 368385.
[pdf]
Abstract: Coalgebraic logic has been mostly developed for coalgebras over sets. This paper studies how
some wellknown 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 Typed Lambda Calculi and Applications 2011 (Springer LNCS 6690), pp. 4560.
[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.