Chris Kapulkin - Publications & Preprints

Back to main page


  1. The Homotopy Theory of Type Theories, with Peter LeFanu Lumsdaine
    Preprint, 2016. [pdf] [arXiv]

  2. Locally Cartesian Closed Quasicategories from Type Theory
    Submitted, 2015. [pdf] [arXiv] [youtube]

  3. Quasicategories of frames of cofibration categories, with Karol Szumiło
    Applied Categorical Structures Online First, February 2016. [website] [pdf] [arXiv]

  4. Joyal's Conjecture in Homotopy Type Theory
    Ph.D. Thesis, 2014. [award]

  5. Homotopy type theory, as part of the Univalent Foundations Project
    Book, 2013. [website] [arXiv]

  6. Homotopy limits in type theory, with Jeremy Avigad and Peter LeFanu Lumsdaine
    Math. Structures Comput. Sci. 25 (2015), no. 5, 1040–1070. [pdf] [Coq] [arXiv]

  7. Univalent categories and Rezk completion, with Benedikt Ahrens and Mike Shulman
    Math. Structures Comput. Sci. 25 (2015), no. 5, 1010–1039. [pdf] [Coq] [arXiv]

  8. The Simplicial Model of Univalent Foundations (after Voevodsky), with Peter LeFanu Lumsdaine
    Preprint, 2012. [pdf] [arXiv]

  9. Univalence in Simplicial Sets, with Peter LeFanu Lumsdaine and Vladimir Voevodsky
    Preprint, 2012. [pdf] [arXiv]

  10. Expressivness of positive coalgebraic logic, with Alexander Kurz and Jiri Velebil
    Advances in modal logic. Vol. 9, 368–385, Coll. Publ., London, 2012. [pdf]

  11. Homotopy theoretic models of type theory, with Peter Arndt
    Typed lambda calculi and applications, 45–60,
    Lecture Notes in Comput. Sci., 6690, Springer, Heidelberg, 2011. [pdf] [arXiv]

See also: Google Scholar, arXiv, MathSciNet.


Updated by Chris Kapulkin, October 3rd, 2016.