Nicolai Kraus
University of Nottingham
I am a Royal Society University Research Fellow 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, and the vast area of related topics.
Feel free to contact me:
firstname.lastname@nottingham.ac.uk.
Quick links:
Papers;
Workshop Contributions;
Talks;
Teaching;
Notes;
Funding Acknowledgement;
and a list of bibtex entries for my papers [html].
Papers

Coherence via Wellfoundedness: Taming SetQuotients in Homotopy Type Theory
[arxiv]
[bibtex]

TwoLevel Type Theory and Applications
[arxiv]
[bibtex]

Shallow Embedding of Type Theory is Morally Correct
[arxiv]
[Agda (bitbucket)]
[bibtex]

MPC'19.

With Ambrus Kaposi and András Kovács.

From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
[arxiv]
[bibtex]

Path Spaces of Higher Inductive Types in Homotopy Type Theory
[arxiv]
[bibtex]

Free Higher Groups in Homotopy Type Theory [arxiv][acm]
[bibtex]

Quotient inductiveinductive types [arxiv]
[bibtex]

FoSSaCS'18.

With Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg.

Univalent Higher Categories via Complete SemiSegal Types [arxiv (full version)] [acm]
[bibtex]

SpaceValued Diagrams, TypeTheoretically (Extended Abstract) [arxiv]
[bibtex]

Partiality, Revisited: The Partiality Monad as a Quotient InductiveInductive Type [Springer][arxiv][acm]
[bibtex]

Extending Homotopy Type Theory With Strict Equality [pdf in the proceedings][arxiv]
[bibtex]

With Thorsten Altenkirch and Paolo Capriotti. CSL'16.

Constructions with NonRecursive Higher Inductive Types [pdf][acm]
[bibtex]

Functions out of Higher Truncations [dagstuhl][arXiv]
[bibtex]

With Paolo Capriotti and Andrea Vezzosi. CSL'15.

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).

The General Universal Property of the Propositional Truncation [dagstuhl][newest version: arXiv]
[bibtex]

Notions of Anonymous Existence in MartinLöf Type Theory [arxiv]
[bibtex]

Higher Homotopies in a Hierarchy of Univalent Universes
[acm]
[arXiv]
[bibtex]

Generalizations of Hedberg’s Theorem [pdf][html on ME's website][blog post]
[bibtex]

With Martin Escardo, Thierry Coquand and Thorsten Altenkirch. TLCA'13.

The final publication is available at link.springer.com.

A Lambda Term Representation Inspired by Linear Ordered Logic [arXiv]
[bibtex]
PeerReviewed Workshop Contributions

An Induction Principle for Cycles [pdf]  at TYPES 2020.

On Symmetries of Spheres in HoTTUF [pdf]  at TYPES 2020.

With Pierre Cagne and Marc Bezem.

Shallow Embedding of Type Theory is Morally Correct [pdf]  at TYPES 2020.

With Ambrus Kaposi and András Kovács.

Twisted Cubes via Graph Morphisms [pdf, book of abstracts]  at TYPES 2019.

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.

Specifying Quotient InductiveInductive Types [book of abstracts]  at TYPES 2018 with Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg.

Formalisations Using TwoLevel Type Theory [pdf]  at HoTT/UF 2017 with Danil Annenkov and Paolo Capriotti.

Type Theory with Weak J [pdf]  at TYPES 2017 with Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, and Simon Huber.

NonRecursive Truncations [pdf]  at TYPES 2016.

I mainly compare different constructions of the propositional truncation.

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 infinitysemicategory in order to organise towers of coherences.

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.

Eliminating out of Truncations [pdf]  at HoTT/UF in Warsaw, April 2015.

Eliminating Higher Truncations via Constancy [pdf]
 at TYPES 2014 with Paolo Capriotti

We generalise the universal property of ntruncations.

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
Below are slides, abstract, or descriptions of some of my talks. Many of my talks are boardbased.

Induction for Cycles [slides]

Coherence via Wellfoundedness [conference abstract]

FAUM (Foundations and Applications of Univalent Mathematics), Herrsching, 18 December 2019.

Internal highercategorical models of dependent type theory
[abstract]

Lab Lunch, Birmingham, 24 October 2019.

Constructive Ordinals

FP Lunch, Nottingham, 18 October 2019.

Higher Type Theory [repository]

Budapest Type Theory Seminar, 9 September 2019.

Homotopical ideas in type theory [conference website and abstract]

Types in Munich, Munich, 7 June 2019.

Deep and shallow embedding of groups [greenboard pictures]

Budapest Type Theory Seminar, 13 May 2019.

Some connections between open problems [slides][video]

Free Higher Groups in Homotopy Type Theory [slides]

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.)

The Role of Semisimplicial Types [slides]

The Challenge of Free Groups, or: Are certain types inhabitable in some but not all versions of HoTT? [video]

An Introduction to 2LTT

Chalmers Prolog Meeting, Gothenburg Cambridge Category Theory Seminar, May 2018,

Towards infinitycategories in type theory

Chalmers Prolog Meeting, Gothenburg Cambridge Category Theory Seminar, May 2018,

Univalent Higher Categories via Complete SemiSegal Types [slides][video]

At POPL'18 in Los Angeles, 10 January 2018.

TwoLevel Type Theory [abstract]

Cambridge Category Theory Seminar, 7 November 2017, organised by Tamara von Glehn.

Type Theory with Weak J [slides]

Higher Categorical Structures, TypeTheoretically [slides][abstract]

Cambridge Logic and Semantics Seminar, 12 May 2017, organised by Dominic Mulligan.

Caveat: This talk was mostly whiteboardbased, and I covered only a tiny part of the contents on the slides.

Partiality, Revisited: The Partiality Monad as a Quotient InductiveInductive Type [slides]

Truncation Levels in Homotopy Type Theory  Ackermann Award Talk [slides]

Higher Categorical Structures and Homotopy Coherent Diagrams

Constructions with NonRecursive Higher Inductive Types [slides]

NonRecursive Truncations [slides]

Talk at TYPES'16 in Novi Sad, 25 May 2016.

NonRecursive Higher Inductive Types [slides]

Higher Inductive Types without Recursive Higher Constructors [slides]

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.)

Eliminating out of Truncations [slides]

Omega Constancy and Truncations [slides]

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).

Universe n is not an nType

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 UFwiki.

Abstract.

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.

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.

Equality in the Dependently Typed Lambda Calculus: An Introduction to Homotopy Type Theory [slides]

Homotopy Type Theory [slides]

Talk for the FP Away Day 2011 in Buxton  just a presentation of very basic ideas and intuition.

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.
Teaching

Introduction to homotopy type theory [course website]  a course at the EU Types summer school that I have given in Ohrid, August/September 2019.

Mathematical Foundations of Programming (G54FOP) and the Foundations Mini Project (G54FPP) [course website]  an MSc/fourth year course at the University of Nottingham.

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].

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 and Reports

A Haskell script to generate the type of ntruncated semisimplicial types [Haskell] [Agda]

One can use the Haskell script to generate Agda code for ntruncated semisimplicial types. To typecheck, 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.

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.

1Types and SetBased Groupoids [pdf]

We compare two notions of groupoids: 1types, and the one of a set of objects, together with sets of homset (indexed over the objects).

NonNormalizability 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 Cauchyreal into a discrete type are constant.

Some Families of Categories with Propositional HomSets [pdf]

A list defining complete partial orders, Heyting algebras and so on in terms of categories, to make up for my memory.

Setoids are not an LCCC [pdf]

With Thorsten Altenkirch. A short proof of the wellknown fact that neither the category of small groupoids nor its full subcategory of setoids is locally cartesian closed.

Yoneda Groupoids [pdf]

My Yoneda Groupoids are special weak omega groupoids that have a simple and short formalisation.

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).

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).

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".

On String Rewriting Systems (draft) [pdf]

Unfinished draft, joint work with Christian Sattler, to tackle an open problem on onerule 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
My work is supported by