Chris Kapulkin - Publications & Preprints

Back to main page


  1. 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 reasoning--but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.

  2. Homotopy limits in type theory, with Jeremy Avigad and Peter Lumsdaine
    Accepted for publication, 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.

  3. 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 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.

  4. The Simplicial Model of Univalent Foundations, with Peter Lumsdaine and Vladimir Voevodsky
    Submitted, 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.

  5. Expressivness of positive coalgebraic logic, with Alexander Kurz and Jiri Velebil
    In Advances in Modal Logic vol. 9, 2012, pp. 368-385. [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.

  6. Homotopy theoretic models of type theory, with Peter Arndt
    In Typed Lambda Calculi and Applications 2011 (Springer LNCS 6690), pp. 45-60.
    [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.


Updated by Chris Kapulkin, June 27th, 2014.