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

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.

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. On symmetries of spheres in univalent foundations [ACM] [arxiv] [bibtex]
   • LICS'24.
   • With Pierre Cagne, Ulrik Buchholtz, and Marc Bezem.
2. Set-Theoretic and Type-Theoretic Ordinals Coincide [IEEE] [arxiv] [bibtex] [Agda (html)]
   • LICS'23.
   • With Tom de Jong, Fredrik Nordvall Forsberg, and Chuangjie Xu.
   • Note on the Agda source code: Part 1 is included in Martín Escardó's TypeTopology library, and Part 2 is included in our constructive ordinals in HoTT project.
3. Type-Theoretic Approaches to Ordinals [TCS] [arxiv] [bibtex] [Agda (source)] [Agda (html)]
   • Theoretical Computer Science.
   • With Fredrik Nordvall Forsberg and Chuangjie Xu.
   • This paper improves and expands on the constructions of "Connecting Constructive Notions of Ordinals in Homotopy Type Theory".
   • Caveat: In the published version (TCS), Theorem 73 uses an unnecessary assumption and Theorem 74 is incorrect. This is corrected in the arXiv version.
4. A Rewriting Coherence Theorem with Applications in Homotopy Type Theory [arxiv] [bibtex] [journal]
   • Mathematical Structures in Computer Science.
   • With Jakob von Raumer.
   • Note: This paper presents some of the ideas of "Coherence via Wellfoundedness" (see below) in the language of higher-dimensional rewriting.
5. Connecting Constructive Notions of Ordinals in Homotopy Type Theory [LIPIcs] [arxiv (includes proofs)] [bibtex] [Agda (source)] [Agda (html)]
   • MFCS'21.
   • With Fredrik Nordvall Forsberg and Chuangjie Xu. Note: This paper is superseded by "Type-Theoretic Approaches to Ordinals".
6. 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)]
   • LICS'21.
   • The Agda formalisation linked above contains a mechanisation of idempotent equivalences.
7. Coherence via Wellfoundedness: Taming Set-Quotients in Homotopy Type Theory [acm] [arxiv] [bibtex]
   • LICS'20.
   • With Jakob von Raumer. Lean formalisation on GitLab.
   • Note: A possibly better presentation of the ideas in this paper can be found in "A Rewriting Coherence Theorem with Applications in Homotopy Type Theory" (see above).
8. Two-Level Type Theory and Applications [journal] [arxiv] [bibtex]
   • Mathematical Structures in Computer Science.
   • With Danil Annenkov, Paolo Capriotti, and Christian Sattler. Lean formalisation on GitHub.
9. Shallow Embedding of Type Theory is Morally Correct [Springer] [arxiv] [Agda (bitbucket)] [bibtex]
   • MPC'19.
   • With Ambrus Kaposi and András Kovács.
10. From Cubes to Twisted Cubes via Graph Morphisms in Type Theory [LIPIcs] [arxiv] [bibtex]
    • With Gun Pinyo.
11. Path Spaces of Higher Inductive Types in Homotopy Type Theory [IEEE] [arxiv] [bibtex]
    • LICS'19.
    • With Jakob von Raumer.
12. Free Higher Groups in Homotopy Type Theory [ACM] [arxiv] [bibtex]
    • LICS'18.
    • With Thorsten Altenkirch.
13. Quotient inductive-inductive types [Springer] [arxiv] [bibtex]
    • FoSSaCS'18.
    • With Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg.
14. Univalent Higher Categories via Complete Semi-Segal Types [ACM] [arxiv (full version)] [bibtex]
    • POPL'18.
    • With Paolo Capriotti. Agda formalisation on GitLab and as html.
15. Space-Valued Diagrams, Type-Theoretically (Extended Abstract) [arxiv] [bibtex]
    • With Christian Sattler.
16. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [Springer] [arxiv] [ACM] [bibtex]
    • With Thorsten Altenkirch and Nils Anders Danielsson. FoSSaCS'17.
    • The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-54458-7_31.
17. Extending Homotopy Type Theory With Strict Equality [Dagstuhl] [arxiv] [bibtex]
    • With Thorsten Altenkirch and Paolo Capriotti. CSL'16.
18. Constructions with Non-Recursive Higher Inductive Types [ACM] [pdf] [bibtex]
    • LICS'16.
    • You can find an Agda formalisation on GitHub, alternatively as html here.
19. Functions out of Higher Truncations [dagstuhl] [arXiv] [bibtex]
    • With Paolo Capriotti and Andrea Vezzosi. CSL'15.
20. Truncation Levels in Homotopy Type Theory [pdf] [formalisation (html)] [formalisation (source, zip)] [bibtex]
    • PhD thesis, University of Nottingham 2015, won the Ackermann award (report by Thierry Coquand and Anuj Dawar).
    • Advisor: Thorsten Altenkirch. Examiners: Julie Greemsmith (internal) and Steve Awodey (external).
21. The General Universal Property of the Propositional Truncation [dagstuhl] [newest version: arXiv] [bibtex]
    • Post-proceedings of TYPES'14.
22. Notions of Anonymous Existence in Martin-Löf Type Theory [LMCS] [arxiv] [bibtex]
    • With Martín Escardó, Thierry Coquand and Thorsten Altenkirch. Logical Methods in Computer Science, our contribution to the special issue of TLCA'13.
    • The formalisation is on GitHub, but it is also contained in my thesis formalisation as html.
23. Higher Homotopies in a Hierarchy of Univalent Universes [ACM] [arXiv] [bibtex]
    • With Christian Sattler. Transactions on Computational Logic.
24. Generalizations of Hedberg’s Theorem [Springer] [pdf] [html on ME's website] [blog post] [bibtex]
    • With Martín Escardó, Thierry Coquand and Thorsten Altenkirch. TLCA'13.
    • The final publication is available at link.springer.com.
25. A Lambda Term Representation Inspired by Linear Ordered Logic [arXiv] [bibtex]
    • With Andreas Abel. LFMTP 2011.

Peer-Reviewed Workshop Contributions

1. The ordinals in set theory and type theory are the same [pdf] - at TYPES 2023.
   • With Tom de Jong, Fredrik Nordvall Forsberg, and Chuangjie Xu.
2. Categories as Semicategories with Identities [pdf] - at TYPES 2023.
   • With Joshua Chen, Tom de Jong, and Stiéphen Pradal.
3. Relating ordinals in set theory to ordinals in type theory [pdf] - at HoTT/UF 2023 and Homotopy Type Theory 2023.
   • With Tom de Jong, Fredrik Nordvall Forsberg, and Chuangjie Xu.
4. Constructivity Aspects of Brouwer Tree Ordinals [pdf] - at Continuity, Computability, Constructivity.
   • With Fredrik Nordvall Forsberg and Chuangjie Xu.
5. Decidability and Semidecidability via Ordinals [pdf] - at TYPES 2022.
   • With Fredrik Nordvall Forsberg and Chuangjie Xu.
6. Wellfounded and Extensional Ordinals in Homotopy Type Theory [conference proceedings pdf] - at DCS (Developments in Computer Science).
   • Not peer-reviewed (invited contribution).
7. A Certified Library of Ordinal Arithmetic [pdf] - at CCC 2021.
   • With Fredrik Nordvall Forsberg and Chuangjie Xu.
8. Syntax for two-level type theory [pdf] - at HoTT/UF 2021.
   • With Roberta Bonacina and Benedikt Ahrens.
9. Semisimplicial Types in Internal Categories with Families [pdf] - at TYPES 2021.
   • With Joshua Chen.
10. Constructive Notions of Ordinals in Homotopy Type Theory [pdf] - at TYPES 2021.
    • With Fredrik Nordvall Forsberg and Chuangjie Xu.
11. An Induction Principle for Cycles [pdf] - at TYPES 2020.
    • With Jakob von Raumer.
12. On Symmetries of Spheres in HoTT-UF [pdf] - at TYPES 2020.
    • With Pierre Cagne and Marc Bezem.
13. Shallow Embedding of Type Theory is Morally Correct [pdf] - at TYPES 2020.
    • With Ambrus Kaposi and András Kovács.
14. Twisted Cubes via Graph Morphisms [pdf, book of abstracts] - at TYPES 2019.
    • With Gun Pinyo.
15. On the Role of Semisimplicial Types [pdf, book of abstracts] - at TYPES 2018.
    • Some reasons why I believe that the open problem of defining semisimplicial types is important.
16. Specifying Quotient Inductive-Inductive Types [book of abstracts] - at TYPES 2018.
    • With Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg.
17. Formalisations Using Two-Level Type Theory [pdf] - at HoTT/UF 2017.
    • With Danil Annenkov and Paolo Capriotti.
18. Type Theory with Weak J [pdf] - at TYPES 2017.
    • With Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, and Simon Huber.
19. Non-Recursive Truncations [pdf] - at TYPES 2016.
    • I mainly compare different constructions of the propositional truncation.
20. Higher Categories in Homotopy Type Theory [pdf] - at TYPES 2016.
    • With Thorsten Altenkirch and Paolo Capriotti. We describe how we want to use a suitable notion of infinity-semicategory in order to organise towers of coherences.
21. Infinite Structures in Type Theory: Problems and Approaches [pdf] - at TYPES 2015.
    • With Thorsten Altenkirch and Paolo Capriotti. We discuss constructions that are desirable but cannot be performed in HoTT.
22. Eliminating out of Truncations [pdf] - at HoTT/UF in Warsaw, April 2015.
    • The "Čech nerve formula" for the (-1)-truncation and related results for higher truncations.
23. Eliminating Higher Truncations via Constancy [pdf] - at TYPES 2014.
    • With Paolo Capriotti. We generalise the universal property of n-truncations.
24. Isomorphism of Finitary Inductive Types [pdf] - at TYPES 2014.
    • With Christian Sattler. We present an algorithm for deciding isomorphism of finitary inductive types.

Some of My Talks

1. Programs as Proofs (and why some computer scientists nowadays do homotopy theory) [abstract]
   • At the University of Aberdeen, 5 June 2023.
2. Decidability and Semidecidability via ordinals [slides]
   • At TYPES'22, Nantes, 20-25 June 2022.
3. Identities in higher categories [slides]
   • At Logic and Higher Structures, CIRM Luminy, 21-25 February 2022.
4. Connecting Constructive Notions of Ordinals in Homotopy Type Theory [slides]
   • At MFCS'21, Tallinn/online, 23-27 August 2021.
5. Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT [slides][youtube]
   • At LICS'21, Rome/online, 29 June - 2 July 2021.
6. Wellfounded and Extensional Ordinals in Homotopy Type Theory [annotated slides]
   • At Developments in Computer Science, Budapest/online, 17-19 June 2021.
7. Constructive Notions of Ordinals in Homotopy Type Theory [slides] [youtube]
   • Joint talk with Fredrik Nordvall Forsberg and Chuangjie Xu. At TYPES'21, Leiden/online, 14-18 June 2021.
8. Internal ∞-Categories with Families [slides]
   • At Strathclyde's MSP 101 Seminar, 18 February 2021.
   • Note: I have given another talk on the topic at Pittsburgh's HoTT Seminar on 9 October 2020.
9. Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it? [annotated slides]
   • At the AIM XXXIII, 20 October 2020.
10. Induction for Cycles [slides]
    • At the Birmingham Theory Seminar, 31 January 2020;
    • also at Types in Munich, replaced by an online conference, 11 March 2020;
    • also at the Budapest type theory seminar, held online, 17 March 2020.
    • A similar talk at FP lunch Nottingham, 24 April 2020: "whiteboard" picture
11. Coherence via Wellfoundedness [conference abstract]
    • FAUM (Foundations and Applications of Univalent Mathematics), Herrsching, 18 December 2019.
12. Internal higher-categorical models of dependent type theory [abstract]
    • Lab Lunch, Birmingham, 24 October 2019.
13. Constructive Ordinals
    • FP Lunch, Nottingham, 18 October 2019.
14. Higher Type Theory [repository]
    • Budapest Type Theory Seminar, 9 September 2019.
15. Homotopical ideas in type theory [conference website and abstract]
    • Types in Munich, Munich, 7 June 2019.
16. Deep and shallow embedding of groups [greenboard pictures]
    • Budapest Type Theory Seminar, 13 May 2019.
17. Some connections between open problems [slides][video]
    • At Homotopy Type Theory Electronic Seminar Talks (HoTTEST), expert level seminar, online, hosted by Chris Kapulkin and Dan Christensen at the University of Western Ontario, 25 October 2018.
18. Free Higher Groups in Homotopy Type Theory [slides]
    • At LICS'18, Oxford, 9 July 2018.
19. Towards the Syntax and Semantics of Higher Dimensional Type Theory [slides]
    • At HoTT/UF'18, Oxford, 8 July 2018.
      (I have given this talk for Thorsten Altenkirch, who was unable to attend.)
20. On the Role of Semisimplicial Types [slides]
    • At TYPES'18, Braga, 18 June 2018.
21. The Challenge of Free Groups, or: Are certain types inhabitable in some but not all versions of HoTT? [video]
    • At the Types, Homotopy Type theory, and Verification workshop at the Hausdorff Institute for Mathematics in Bonn, 8 June 2018.
22. An Introduction to 2LTT
    • Chalmers Seminar, Gothenburg, May 2018.
23. Towards infinity-categories in type theory
    • Chalmers Prolog Meeting, Gothenburg, May 2018.
24. Univalent Higher Categories via Complete Semi-Segal Types [slides][video]
    • At POPL'18 in Los Angeles, 10 January 2018.
25. Two-Level Type Theory [abstract]
    • Cambridge Category Theory Seminar, 7 November 2017, organised by Tamara von Glehn.
26. Type Theory with Weak J [slides]
    • At TYPES'17 in Budapest, 1 June 2017.
27. Higher Categorical Structures, Type-Theoretically [slides][abstract]
    • Cambridge Logic and Semantics Seminar, 12 May 2017, organised by Dominic Mulligan.
    • Caveat: This talk was mostly whiteboard-based, and I covered only a tiny part of the contents on the slides.
28. Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [slides]
    • At FoSSaCS'17 (part of ETAPS) in Uppsala, 26 April 2017.
29. Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
    • At CSL'16 in Marseille, 31 August 2016 (CSL event).
30. Higher Categorical Structures and Homotopy Coherent Diagrams
    • Talk at the workshop on categorical logic and univalent foundations in Leeds, 27 July 2016.
    • I did not use slides, but Ulrik Buchholtz wrote some notes on facebook - many thanks, Ulrik!
    • Here are all the abstracts.
31. Constructions with Non-Recursive Higher Inductive Types [slides]
    • LICS'16 in New York, 6 July 2016.
32. Non-Recursive Truncations [slides]
    • Talk at TYPES'16 in Novi Sad, 25 May 2016.
33. Non-Recursive Higher Inductive Types [slides]
    • Talk at the HoTT/UF workshop at Fields in Toronto, 20 May 2016.
    • You can find video recordings of the talks at this event here.
34. Higher Inductive Types without Recursive Higher Constructors [slides]
    • Talk at the MGS Christmas Seminar in Birmingham, 17 December 2015.
35. Functions out of Higher Truncations [slides]
    • Talk at CSL'15 in Berlin, 8 September 2015.
    • (The content of this talk is different from that of the talk below, although the titles are very similar.)
36. Eliminating out of Truncations [slides]
    • Talk at the HoTT/UF workshop in Warsaw, 30 June 2015.
37. Omega Constancy and Truncations [slides]
    • My talk for the FP Away Day 2014 in Buxton, July 2014.
38. Generalizations of Hedberg's Theorem [slides]
    • My talk at TLCA in Eindhoven, June 2013.
    • I have given a similar talk with the same title at the FP Away Day in Buxton, June 2013 (the original slides are on the event homepage).
39. Universe n is not an n-Type
    • Talk at the Univalent Foundations Program at the IAS in Princeton, April 2013. No slides available, but there are some notes to the talk on the UF-wiki.
    • Abstract.
40. Homotopy Type Theory and Hedberg's Theorem [slides]
    • Talk for my visit in Birmingham, November 2012. Based on joint work with T. Altenkirch, T. Coquand, M. Escardo. Abstract.
41. On Hedberg's theorem: Proving and Painting [slides]
    • My talk for the FP Away Day 2012 in Hathersage.
    • An attempt to provide some more intuition for HoTT, together with Hedberg's theorem as an application.
42. Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]
    • Talk at Computing 2011, Karlsruhe.
    • Abstract.
43. Homotopy Type Theory [slides]
    • Talk for the FP Away Day 2011 in Buxton - just a presentation of very basic ideas and intuition.
44. A Lambda Term Representation Inspired by Linear Ordered Logic [slides]
    • My talk at the workshop LFMTP in Nijmegen, August 2011.
    • I have given a similar talk in February 2011 in Munich, at the LMU TCS seminar.

Events

1. Types, Thorsten and Theories, 12 October 2022.
   • A workshop on type theory in honour of Thorsten Altenkirch's 60th birthday.
2. Midlands Graduate School 22, 10-14 April 2022.
   • A spring school on/in the foundations of computing science.
3. MGS Christmas Seminar 2021, 16 December 2021.
   • The annual MGS Christmas seminar/celebration.
4. Agda Implementors' Meeting XXVIII, 15-20 October 2018.
   • One of many meetings for Agda developers and users.

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

1. A Haskell script to generate the type of n-truncated semi-simplicial types [Haskell] [Agda]
   • One can use the Haskell script to generate Agda code for n-truncated semi-simplicial types. To type-check, the strings can be copied into the Agda file.
   • However, this is really only a proof of concept and could be done much more professionally. (2014, see Section 9.2 of my PhD thesis.)
2. The Truncation Map on Nat is Nearly Invertible [blog post], Agda formalisation and explanation [html]
   • We construct a term which looks like an inverse of the truncation projection Nat -> ||Nat||. (2013, see Section 6.4 of my PhD thesis.)
3. 1-Types and Set-Based Groupoids [pdf]
   • We compare two notions of groupoids: 1-types, and the one of a set of objects, together with sets of hom-set indexed over the objects. (See Section 9.4 of my PhD thesis.)
4. Non-Normalizability of Cauchy Sequences [pdf]
   • We prove that there is no definable (or continuous) endofunction on the set of Cauchy sequences such that f(s)~s and s~t -> f(s)=f(t), where s~t means that the difference of the Cauchy sequences s and t converges to 0. In general, all definable functions from the Cauchy-real into a discrete type are constant.
5. Some Families of Categories with Propositional Hom-Sets [pdf]
   • A list defining complete partial orders, Heyting algebras and so on in terms of categories, to make up for my memory.
6. Setoids are not an LCCC [pdf]
   • With Thorsten Altenkirch. A short proof of the well-known fact that neither the category of small groupoids nor its full subcategory of setoids is locally cartesian closed.
7. Yoneda Groupoids [pdf]
   • My Yoneda Groupoids are special weak omega groupoids that have a simple and short formalisation. (See Section 9.3 of my PhD thesis.)
8. First year report [pdf], and extended version [pdf]
   • In the shorter version, mainly those contents that are not central to HoTT are left out. (Note on the extended version: for the part about Yoneda Groupoids I would recommend to look at the separate note above).
9. Homotopy Type Theory - An overview [pdf]
   • My introduction to HoTT (also the main part of my first year report). Caveat: When I wrote this, I was quite new to HoTT and teaching it to myself. Today, there are certainly better introductions (in particular the book, although I tried to explain a bit about models, which the book does not).
10. A direct proof of Hedberg's theorem in Coq [Coq], see also my post on the HoTT blog [website]
    • A variant of the proof of Hedberg's theorem. Includes a slight improvement, namely "local decidability implies local UIP".
11. On String Rewriting Systems (draft) [pdf]
    • Unfinished draft, joint work with Christian Sattler, to tackle an open problem on one-rule string rewriting systems (see the RTA open problems list).
    • Our techniques are not sufficient to solve the problem and (we think) are already known.

Funding Acknowledgement

I am generously supported by