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

Some of My Talks

  1. Type Theory with Weak J [slides]
  2. Higher Categorical Structures, Type-Theoretically [slides]
  3. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [slides]
  4. Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
  5. Higher Categorical Structures and Homotopy Coherent Diagrams
  6. Constructions with Non-Recursive Higher Inductive Types [slides]
  7. Non-Recursive Truncations [slides]
  8. Non-Recursive Higher Inductive Types [slides]
  9. Higher Inductive Types without Recursive Higher Constructors [slides]
  10. Functions out of Higher Truncations [slides]
  11. Eliminating out of Truncations [slides]
  12. Omega Constancy and Truncations [slides]
  13. Generalizations of Hedberg's Theorem [slides]
  14. Universe n is not an n-Type
  15. Homotopy Type Theory and Hedberg's Theorem [slides]
  16. On Hedberg's theorem: Proving and Painting [slides]
  17. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]
  18. Homotopy Type Theory [slides]
  19. A Lambda Term Representation Inspired by Linear Ordered Logic [slides]

Teaching

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