Nicolai Kraus

Professor of Theoretical Computer Science
Royal Society University Research Fellow
University of Nottingham

Nicolai Kraus

Welcome to by website! I am a Royal Society University Research Fellow and Professor of Theoretical Computer Science 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.

I am working in the area of dependent type theory (favourite proof assistant: Agda), for which I will from 2025 lead an ERC (European Research Council) project. My main focus is homotopy type theory and (higher) categories, but I like to think about topics and questions in constructive or non-constructive mathematics in general.

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

People

I am currently supervising and working with:
  1. Aref Mohammadzadeh, who started his PhD with me in December 2024.
  2. Tom de Jong, who started as a postdoc with me in October 2022.
  3. Stiéphen Pradal, who started his PhD with me in October 2022.
  4. Joshua Chen, working on his PhD with me since October 2020.
I am also the second supervisor of:
  1. Johannes Schipp von Branitz, working on his PhD with Ulrik Buchholtz since October 2022.
  2. Stefania Damato, who started her PhD with Thorsten Altenkirch in October 2021.

Papers

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

Peer-Reviewed Workshop Contributions

  1. Constructive Ordinal Exponentiation in Homotopy Type Theory [pdf] - at TYPES 2024.
  2. The ordinals in set theory and type theory are the same [pdf] - at TYPES 2023.
  3. Categories as Semicategories with Identities [pdf] - at TYPES 2023.
  4. Relating ordinals in set theory to ordinals in type theory [pdf] - at HoTT/UF 2023 and Homotopy Type Theory 2023.
  5. Constructivity Aspects of Brouwer Tree Ordinals [pdf] - at Continuity, Computability, Constructivity.
  6. Decidability and Semidecidability via Ordinals [pdf] - at TYPES 2022.
  7. Wellfounded and Extensional Ordinals in Homotopy Type Theory [conference proceedings pdf] - at DCS (Developments in Computer Science).
  8. A Certified Library of Ordinal Arithmetic [pdf] - at CCC 2021.
  9. Syntax for two-level type theory [pdf] - at HoTT/UF 2021.
  10. Semisimplicial Types in Internal Categories with Families [pdf] - at TYPES 2021.
  11. Constructive Notions of Ordinals in Homotopy Type Theory [pdf] - at TYPES 2021.
  12. An Induction Principle for Cycles [pdf] - at TYPES 2020.
  13. On Symmetries of Spheres in HoTT-UF [pdf] - at TYPES 2020.
  14. Shallow Embedding of Type Theory is Morally Correct [pdf] - at TYPES 2020.
  15. Twisted Cubes via Graph Morphisms [pdf, book of abstracts] - at TYPES 2019.
  16. On the Role of Semisimplicial Types [pdf, book of abstracts] - at TYPES 2018.
  17. Specifying Quotient Inductive-Inductive Types [book of abstracts] - at TYPES 2018.
  18. Formalisations Using Two-Level Type Theory [pdf] - at HoTT/UF 2017.
  19. Type Theory with Weak J [pdf] - at TYPES 2017.
  20. Non-Recursive Truncations [pdf] - at TYPES 2016.
  21. Higher Categories in Homotopy Type Theory [pdf] - at TYPES 2016.
  22. Infinite Structures in Type Theory: Problems and Approaches [pdf] - at TYPES 2015.
  23. Eliminating out of Truncations [pdf] - at HoTT/UF in Warsaw, April 2015.
  24. Eliminating Higher Truncations via Constancy [pdf] - at TYPES 2014.
  25. Isomorphism of Finitary Inductive Types [pdf] - at TYPES 2014.

Some of My Talks

If you're looking for a specific talk and it's missing, please let me know. Maybe I didn't have anything to put online (for example if the talk was board-based), but it's at least as likely that I just forgot.
  1. Two-level type theory [slides]
  2. Programs as Proofs (and why some computer scientists nowadays do homotopy theory) [abstract]
  3. Decidability and Semidecidability via ordinals [slides]
  4. Identities in higher categories [slides]
  5. Connecting Constructive Notions of Ordinals in Homotopy Type Theory [slides]
  6. Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT [slides][youtube]
  7. Wellfounded and Extensional Ordinals in Homotopy Type Theory [annotated slides]
  8. Constructive Notions of Ordinals in Homotopy Type Theory [slides] [youtube]
  9. Internal ∞-Categories with Families [slides]
  10. Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it? [annotated slides]
  11. Induction for Cycles [slides]
  12. Coherence via Wellfoundedness [conference abstract]
  13. Internal higher-categorical models of dependent type theory [abstract]
  14. Constructive Ordinals
  15. Higher Type Theory [repository]
  16. Homotopical ideas in type theory [conference website and abstract]
  17. Deep and shallow embedding of groups [greenboard pictures]
  18. Some connections between open problems [slides][video]
  19. Free Higher Groups in Homotopy Type Theory [slides]
  20. Towards the Syntax and Semantics of Higher Dimensional Type Theory [slides]
  21. On the Role of Semisimplicial Types [slides]
  22. The Challenge of Free Groups, or: Are certain types inhabitable in some but not all versions of HoTT? [video]
  23. An Introduction to 2LTT
  24. Towards infinity-categories in type theory
  25. Univalent Higher Categories via Complete Semi-Segal Types [slides][video]
  26. Two-Level Type Theory [abstract]
  27. Type Theory with Weak J [slides]
  28. Higher Categorical Structures, Type-Theoretically [slides][abstract]
  29. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [slides]
  30. Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
  31. Higher Categorical Structures and Homotopy Coherent Diagrams
  32. Constructions with Non-Recursive Higher Inductive Types [slides]
  33. Non-Recursive Truncations [slides]
  34. Non-Recursive Higher Inductive Types [slides]
  35. Higher Inductive Types without Recursive Higher Constructors [slides]
  36. Functions out of Higher Truncations [slides]
  37. Eliminating out of Truncations [slides]
  38. Omega Constancy and Truncations [slides]
  39. Generalizations of Hedberg's Theorem [slides]
  40. Universe n is not an n-Type
  41. Homotopy Type Theory and Hedberg's Theorem [slides]
  42. On Hedberg's theorem: Proving and Painting [slides]
  43. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]
  44. Homotopy Type Theory [slides]
  45. A Lambda Term Representation Inspired by Linear Ordered Logic [slides]

Events

I have organised the following events in Nottingham:
  1. Types, Thorsten and Theories, 12 October 2022.
  2. Midlands Graduate School 22, 10-14 April 2022.
  3. MGS Christmas Seminar 2021, 16 December 2021.
  4. Agda Implementors' Meeting XXVIII, 15-20 October 2018.

Teaching

  1. Category Theory [course website], a course at MGS'23 in Birmingham, 2-6 April 2023.
  2. Homotopy type theory [course website], at MGS 2021, online, 12-16 April 2021.
  3. Introduction to homotopy type theory [course website] - a course at the EU Types summer school that I have given in Ohrid, August/September 2019.
  4. Mathematical Foundations of Programming (G54FOP) and the Foundations Mini Project (G54FPP) [course website] - an MSc/fourth year course at the University of Nottingham.
  5. 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].

Random Notes and Reports

The below list is from my days as a PhD student. Not updated since 2014.
  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


Last updated: August 2024.