Nicolai Kraus

Nicolai Kraus

University of Nottingham

I am a Royal Society University Research Fellow and Associate Professor at the University of Nottingham, in the Functional Programming Lab. I was previously a member of the Birmingham Theory Group and at Eötvös Loránd University. My interests include (homotopy) type theory, (higher) categories, constructive mathematics in general, and the vast area of related topics.

Theoretical Computer Scientists for Future

Feel free to contact me: firstname.lastname@nottingham.ac.uk.

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

People

  1. Joshua Chen started his PhD with me in October 2020.
  2. I am second supervisor of Brandon Hewer, who started his PhD with Graham Hutton in October 2019.

Papers

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

Peer-Reviewed Workshop Contributions

  1. An Induction Principle for Cycles [pdf] - at TYPES 2020.
  2. On Symmetries of Spheres in HoTT-UF [pdf] - at TYPES 2020.
  3. Shallow Embedding of Type Theory is Morally Correct [pdf] - at TYPES 2020.
  4. Twisted Cubes via Graph Morphisms [pdf, book of abstracts] - at TYPES 2019.
  5. On the Role of Semisimplicial Types [pdf, book of abstracts] - at TYPES 2018.
  6. Specifying Quotient Inductive-Inductive Types [book of abstracts] - at TYPES 2018 with Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg.
  7. Formalisations Using Two-Level Type Theory [pdf] - at HoTT/UF 2017 with Danil Annenkov and Paolo Capriotti.
  8. Type Theory with Weak J [pdf] - at TYPES 2017 with Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, and Simon Huber.
  9. Non-Recursive Truncations [pdf] - at TYPES 2016.
  10. Higher Categories in Homotopy Type Theory [pdf] - at TYPES 2016 with Thorsten Altenkirch and Paolo Capriotti
  11. Infinite Structures in Type Theory: Problems and Approaches [pdf] - at TYPES 2015 with Thorsten Altenkirch and Paolo Capriotti
  12. Eliminating out of Truncations [pdf] - at HoTT/UF in Warsaw, April 2015.
  13. Eliminating Higher Truncations via Constancy [pdf] - at TYPES 2014 with Paolo Capriotti
  14. 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. Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it? [annotated slides]
  2. Internal ∞-Categories with Families
  3. Induction for Cycles [slides]
  4. Coherence via Wellfoundedness [conference abstract]
  5. Internal higher-categorical models of dependent type theory [abstract]
  6. Constructive Ordinals
  7. Higher Type Theory [repository]
  8. Homotopical ideas in type theory [conference website and abstract]
  9. Deep and shallow embedding of groups [greenboard pictures]
  10. Some connections between open problems [slides][video]
  11. Free Higher Groups in Homotopy Type Theory [slides]
  12. Towards the Syntax and Semantics of Higher Dimensional Type Theory [slides]
  13. The Role of Semisimplicial Types [slides]
  14. The Challenge of Free Groups, or: Are certain types inhabitable in some but not all versions of HoTT? [video]
  15. An Introduction to 2LTT
  16. Towards infinity-categories in type theory
  17. Univalent Higher Categories via Complete Semi-Segal Types [slides][video]
  18. Two-Level Type Theory [abstract]
  19. Type Theory with Weak J [slides]
  20. Higher Categorical Structures, Type-Theoretically [slides][abstract]
  21. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [slides]
  22. Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
  23. Higher Categorical Structures and Homotopy Coherent Diagrams
  24. Constructions with Non-Recursive Higher Inductive Types [slides]
  25. Non-Recursive Truncations [slides]
  26. Non-Recursive Higher Inductive Types [slides]
  27. Higher Inductive Types without Recursive Higher Constructors [slides]
  28. Functions out of Higher Truncations [slides]
  29. Eliminating out of Truncations [slides]
  30. Omega Constancy and Truncations [slides]
  31. Generalizations of Hedberg's Theorem [slides]
  32. Universe n is not an n-Type
  33. Homotopy Type Theory and Hedberg's Theorem [slides]
  34. On Hedberg's theorem: Proving and Painting [slides]
  35. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]
  36. Homotopy Type Theory [slides]
  37. 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

I am generously supported by

The Royal Society