nicolai kraus

Nicolai Kraus

University of Nottingham

I am a postdoc at 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: nicolai dot kraus at X, where X is either nottingham.ac.uk or gmail.com (more stable). Please do not use my previous Nottingham email addresses psxngk... and ngk... as they have been deactivated!

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

Papers

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

Some of My Talks

  1. Some connections between open problems [slides][video]
  2. Free Higher Groups in Homotopy Type Theory [slides]
  3. Towards the Syntax and Semantics of Higher Dimensional Type Theory [slides]
  4. The Role of Semisimplicial Types [slides]
  5. The Challenge of Free Groups, or: Are certain types inhabitable in some but not all versions of HoTT? [video]
  6. Univalent Higher Categories via Complete Semi-Segal Types [slides][video]
  7. Two-Level Type Theory
  8. Type Theory with Weak J [slides]
  9. Higher Categorical Structures, Type-Theoretically [slides]
  10. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [slides]
  11. Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
  12. Higher Categorical Structures and Homotopy Coherent Diagrams
  13. Constructions with Non-Recursive Higher Inductive Types [slides]
  14. Non-Recursive Truncations [slides]
  15. Non-Recursive Higher Inductive Types [slides]
  16. Higher Inductive Types without Recursive Higher Constructors [slides]
  17. Functions out of Higher Truncations [slides]
  18. Eliminating out of Truncations [slides]
  19. Omega Constancy and Truncations [slides]
  20. Generalizations of Hedberg's Theorem [slides]
  21. Universe n is not an n-Type
  22. Homotopy Type Theory and Hedberg's Theorem [slides]
  23. On Hedberg's theorem: Proving and Painting [slides]
  24. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]
  25. Homotopy Type Theory [slides]
  26. A Lambda Term Representation Inspired by Linear Ordered Logic [slides]

Teaching

  1. Mathematical Foundations of Programming (G54FOP) and the Foundations Mini Project (G54FPP) [course website] - an MSc/fourth year course at the University of Nottingham.
  2. 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].
  3. 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, Workshop Contibutions, Reports

  1. On the Role of Semisimplicial Types [pdf, book of abstracts] - at TYPES 2018.
  2. Specifying Quotient Inductive-Inductive Types [book of abstracts] - at TYPES 2018 with Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg.
  3. Formalisations Using Two-Level Type Theory [pdf] - at HoTT/UF 2017 with Danil Annenkov and Paolo Capriotti.
  4. Type Theory with Weak J [pdf] - at TYPES 2017 with Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, and Simon Huber.
  5. Non-Recursive Truncations [pdf] - at TYPES 2016.
  6. Higher Categories in Homotopy Type Theory [pdf] - at TYPES 2016 with Thorsten Altenkirch and Paolo Capriotti
  7. Infinite Structures in Type Theory: Problems and Approaches [pdf] - at TYPES 2015 with Thorsten Altenkirch and Paolo Capriotti
  8. Eliminating out of Truncations [pdf] - at HoTT/UF in Warsaw, April 2015.
  9. Eliminating Higher Truncations via Constancy [pdf] - at TYPES 2014 with Paolo Capriotti
  10. Isomorphism of Finitary Inductive Types [pdf] - at TYPES 2014 with Christian Sattler
  11. A Haskell script to generate the type of n-truncated semi-simplicial types [Haskell] [Agda]
  12. The Truncation Map on Nat is Nearly Invertible [blog post], Agda formalisation and explanation [html]
  13. 1-Types and Set-Based Groupoids [pdf]
  14. Non-Normalizability of Cauchy Sequences [pdf]
  15. Some Families of Categories with Propositional Hom-Sets [pdf]
  16. Setoids are not an LCCC [pdf]
  17. Yoneda Groupoids [pdf]
  18. First year report [pdf], and extended version [pdf]
  19. Homotopy Type Theory - An overview [pdf]
  20. A direct proof of Hedberg's theorem in Coq [Coq], see also my post on the HoTT blog [website]
  21. On String Rewriting Systems (draft) [pdf]