Nicolai Kraus

University of Nottingham

Nicolai Kraus

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.

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

People

I am currently supervising and working with:
  1. Tom de Jong, who started as a postdoc with me in October 2022.
  2. Stiéphen Pradal, who started his PhD with me in October 2022.
  3. 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.
  3. Brandon Hewer, supervised by Graham Hutton, who started in October 2019.

Papers

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

Peer-Reviewed Workshop Contributions

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

Some of My Talks

Below are slides, abstracts, or descriptions of some of my talks. Many of my talks are board-based.
  1. Decidability and Semidecidability via ordinals [slides]
  2. Identities in higher categories [slides]
  3. Connecting Constructive Notions of Ordinals in Homotopy Type Theory [slides]
  4. Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT [slides][youtube]
  5. Wellfounded and Extensional Ordinals in Homotopy Type Theory [annotated slides]
  6. Constructive Notions of Ordinals in Homotopy Type Theory [slides] [youtube]
  7. Internal ∞-Categories with Families [slides]
  8. Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it? [annotated slides]
  9. Induction for Cycles [slides]
  10. Coherence via Wellfoundedness [conference abstract]
  11. Internal higher-categorical models of dependent type theory [abstract]
  12. Constructive Ordinals
  13. Higher Type Theory [repository]
  14. Homotopical ideas in type theory [conference website and abstract]
  15. Deep and shallow embedding of groups [greenboard pictures]
  16. Some connections between open problems [slides][video]
  17. Free Higher Groups in Homotopy Type Theory [slides]
  18. Towards the Syntax and Semantics of Higher Dimensional Type Theory [slides]
  19. The Role of Semisimplicial Types [slides]
  20. The Challenge of Free Groups, or: Are certain types inhabitable in some but not all versions of HoTT? [video]
  21. An Introduction to 2LTT
  22. Towards infinity-categories in type theory
  23. Univalent Higher Categories via Complete Semi-Segal Types [slides][video]
  24. Two-Level Type Theory [abstract]
  25. Type Theory with Weak J [slides]
  26. Higher Categorical Structures, Type-Theoretically [slides][abstract]
  27. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [slides]
  28. Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
  29. Higher Categorical Structures and Homotopy Coherent Diagrams
  30. Constructions with Non-Recursive Higher Inductive Types [slides]
  31. Non-Recursive Truncations [slides]
  32. Non-Recursive Higher Inductive Types [slides]
  33. Higher Inductive Types without Recursive Higher Constructors [slides]
  34. Functions out of Higher Truncations [slides]
  35. Eliminating out of Truncations [slides]
  36. Omega Constancy and Truncations [slides]
  37. Generalizations of Hedberg's Theorem [slides]
  38. Universe n is not an n-Type
  39. Homotopy Type Theory and Hedberg's Theorem [slides]
  40. On Hedberg's theorem: Proving and Painting [slides]
  41. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]
  42. Homotopy Type Theory [slides]
  43. 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. Note to Nottingham students: All materials for UoN courses (including COMP3012 compilers) are available on Moodle.
  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

  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