Nicolai Kraus

Nicolai Kraus

University of Birmingham

I am a Royal Society University Research Fellow and a lecturer at the University of Birmingham, working as a member of the Birmingham Theory Group. Before that, I was at Eötvös Loránd University. Until early 2019, I was a member of the Functional Programming Lab in Nottingham. My interests include (homotopy) type theory, higher categories, and the vast area of related topics.

Feel free to contact me: n dot kraus at bham dot ac dot uk or nicolai dot kraus at gmail dot com.

Quick links: Papers; Workshop Contributions; Talks; Teaching; Notes; Funding Acknowledgement;
and a list of bibtex entries for my papers [html].

Papers

  1. Coherence via Wellfoundedness: Taming Set-Quotients in Homotopy Type Theory [bibtex]
  2. Two-Level Type Theory and Applications [arxiv] [bibtex]
  3. Shallow Embedding of Type Theory is Morally Correct [arxiv] [Agda (bitbucket)] [bibtex]
  4. From Cubes to Twisted Cubes via Graph Morphisms in Type Theory [arxiv] [bibtex]
  5. Path Spaces of Higher Inductive Types in Homotopy Type Theory [arxiv] [bibtex]
  6. Free Higher Groups in Homotopy Type Theory [arxiv][acm] [bibtex]
  7. Quotient inductive-inductive types [arxiv] [bibtex]
  8. Univalent Higher Categories via Complete Semi-Segal Types [arxiv (full version)] [acm] [bibtex]
  9. Space-Valued Diagrams, Type-Theoretically (Extended Abstract) [arxiv] [bibtex]
  10. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [Springer][arxiv][acm] [bibtex]
  11. Extending Homotopy Type Theory With Strict Equality [pdf in the proceedings][arxiv] [bibtex]
  12. Constructions with Non-Recursive Higher Inductive Types [pdf][acm] [bibtex]
  13. Functions out of Higher Truncations [dagstuhl][arXiv] [bibtex]
  14. Truncation Levels in Homotopy Type Theory [pdf][formalisation (html)][formalisation (source, zip)] [bibtex]
  15. The General Universal Property of the Propositional Truncation [dagstuhl][newest version: arXiv] [bibtex]
  16. Notions of Anonymous Existencs in Martin-Löf Type Theory [arxiv] [bibtex]
  17. Higher Homotopies in a Hierarchy of Univalent Universes [acm] [arXiv] [bibtex]
  18. Generalizations of Hedberg’s Theorem [pdf][html on ME's website][blog post] [bibtex]
  19. A Lambda Term Representation Inspired by Linear Ordered Logic [arXiv] [bibtex]

Peer-Reviewed Workshop Contributions

  1. Twisted Cubes via Graph Morphisms [pdf, book of abstracts] - at TYPES 2019.
  2. On the Role of Semisimplicial Types [pdf, book of abstracts] - at TYPES 2018.
  3. Specifying Quotient Inductive-Inductive Types [book of abstracts] - at TYPES 2018 with Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg.
  4. Formalisations Using Two-Level Type Theory [pdf] - at HoTT/UF 2017 with Danil Annenkov and Paolo Capriotti.
  5. Type Theory with Weak J [pdf] - at TYPES 2017 with Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, and Simon Huber.
  6. Non-Recursive Truncations [pdf] - at TYPES 2016.
  7. Higher Categories in Homotopy Type Theory [pdf] - at TYPES 2016 with Thorsten Altenkirch and Paolo Capriotti
  8. Infinite Structures in Type Theory: Problems and Approaches [pdf] - at TYPES 2015 with Thorsten Altenkirch and Paolo Capriotti
  9. Eliminating out of Truncations [pdf] - at HoTT/UF in Warsaw, April 2015.
  10. Eliminating Higher Truncations via Constancy [pdf] - at TYPES 2014 with Paolo Capriotti
  11. Isomorphism of Finitary Inductive Types [pdf] - at TYPES 2014 with Christian Sattler

Some of My Talks

Below are slides, abstract, or descriptions of some of my talks. Many of my talks are board-based.
  1. Higher Type Theory [conference abstract]
  2. Internal higher-categorical models of dependent type theory [abstract]
  3. Constructive Ordinals
  4. Higher Type Theory [repository]
  5. Homotopical ideas in type theory [conference website and abstract]
  6. Deep and shallow embedding of groups [greenboard pictures]
  7. Some connections between open problems [slides][video]
  8. Free Higher Groups in Homotopy Type Theory [slides]
  9. Towards the Syntax and Semantics of Higher Dimensional Type Theory [slides]
  10. The Role of Semisimplicial Types [slides]
  11. The Challenge of Free Groups, or: Are certain types inhabitable in some but not all versions of HoTT? [video]
  12. An Introduction to 2LTT
  13. Towards infinity-categories in type theory
  14. Univalent Higher Categories via Complete Semi-Segal Types [slides][video]
  15. Two-Level Type Theory [abstract]
  16. Type Theory with Weak J [slides]
  17. Higher Categorical Structures, Type-Theoretically [slides][abstract]
  18. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [slides]
  19. Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
  20. Higher Categorical Structures and Homotopy Coherent Diagrams
  21. Constructions with Non-Recursive Higher Inductive Types [slides]
  22. Non-Recursive Truncations [slides]
  23. Non-Recursive Higher Inductive Types [slides]
  24. Higher Inductive Types without Recursive Higher Constructors [slides]
  25. Functions out of Higher Truncations [slides]
  26. Eliminating out of Truncations [slides]
  27. Omega Constancy and Truncations [slides]
  28. Generalizations of Hedberg's Theorem [slides]
  29. Universe n is not an n-Type
  30. Homotopy Type Theory and Hedberg's Theorem [slides]
  31. On Hedberg's theorem: Proving and Painting [slides]
  32. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]
  33. Homotopy Type Theory [slides]
  34. A Lambda Term Representation Inspired by Linear Ordered Logic [slides]

Teaching

  1. Introduction to homotopy type theory [course website] - a course at the EU Types summer school that I have given in Ohrid, August/September 2019.
  2. Mathematical Foundations of Programming (G54FOP) and the Foundations Mini Project (G54FPP) [course website] - an MSc/fourth year course at the University of Nottingham.
  3. Higher Categories [course website] - a course at MGS'17 that I have given jointly with Paolo Capriotti. There is in particular a guided exercise sheet [pdf].
  4. I have been TA for various lectures from 2009 (Munich) / 2011 (Nottingham). Information for students: Coursework, exercise sheets, solutions, or material discussed in the tutorial are not on this webpage anymore. These can be found on Moodle.

Random Notes and Reports

  1. A Haskell script to generate the type of n-truncated semi-simplicial types [Haskell] [Agda]
  2. The Truncation Map on Nat is Nearly Invertible [blog post], Agda formalisation and explanation [html]
  3. 1-Types and Set-Based Groupoids [pdf]
  4. Non-Normalizability of Cauchy Sequences [pdf]
  5. Some Families of Categories with Propositional Hom-Sets [pdf]
  6. Setoids are not an LCCC [pdf]
  7. Yoneda Groupoids [pdf]
  8. First year report [pdf], and extended version [pdf]
  9. Homotopy Type Theory - An overview [pdf]
  10. A direct proof of Hedberg's theorem in Coq [Coq], see also my post on the HoTT blog [website]
  11. On String Rewriting Systems (draft) [pdf]

Funding Acknowledgement

My work is supported by

The Royal Society