Nicolai Kraus

University of Nottingham


I am a postdoc at the Functional Programming Lab in Nottingham. My main interests are homotopy type theory and the vast area of related topics.

Feel free to contact me: nicolai dot kraus at X, where X is either or (more stable). Please do not use my previous Nottingham email addresses psxngk... and ngk... as they have been deactivated!

Main work

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type [arxiv]
With Thorsten Altenkirch and Nils Anders Danielsson. To be presented at FoSSaCS'17.
Extending Homotopy Type Theory With Strict Equality [pdf in the proceedings][arxiv]
With Thorsten Altenkirch and Paolo Capriotti. CSL'16.
Constructions with Non-Recursive Higher Inductive Types [pdf]
You can find an Agda formalization on GitHub, alternatively as html here.
Functions out of Higher Truncations [dagstuhl][arXiv]
With Paolo Capriotti and Andrea Vezzosi. CSL'15.
Truncation Levels in Homotopy Type Theory [pdf][formalisation (html)][formalisation (source, zip)]
PhD thesis, 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]
Post-proceedings of TYPES'14.
Notions of Anonymous Existencs in Martin-Löf Type Theory [arxiv]
With Martin Escardo, Thierry Coquand and Thorsten Altenkirch. Contribution to the special issue of TLCA'13 (to appear in LMCS). The formalisation is on GitHub, but it is also contained in my thesis formalisation as html.
Higher Homotopies in a Hierarchy of Univalent Universes [ACM library] [arXiv]
With Christian Sattler. Transactions on Computational Logic.
Generalizations of Hedberg’s Theorem [pdf][html on ME's website][blog post]
With Martin Escardo, Thierry Coquand and Thorsten Altenkirch. TLCA'13.
The final publication is available at

Some Talks for which I had slides

Truncation Levels in Homotopy Type Theory - Ackermann Award Talk [slides]
At CSL'16 in Marseille, 31 August 2016 (CSL event).
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.
Constructions with Non-Recursive Higher Inductive Types [slides]
LiCS'16 in New York, 6 July 2016.
Non-Recursive Truncations [slides]
Talk at TYPES'16 in Novi Sad, 25 May 2016.
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 of this event here ("static" version of mine).
Higher Inductive Types without Recursive Higher Constructors [slides]
Talk at the MGS Christmas Seminar in Birmingham, 17 December 2015.
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]
Talk at the HoTT/UF workshop in Warsaw, 30 June 2015.
Omega Constancy and Truncations [slides]
My talk for the FP Away Day 2014 in Buxton, July 2014.
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 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.
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]
Talk at Computing 2011, Karlsruhe. Abstract.
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.

Random Notes, Workshop Contibutions, Reports

Non-Recursive Truncations - at TYPES 2016
I mainly compare different constructions of the propositional truncation.
Higher Categories in Homotopy Type Theory - 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.
Infinite Structures in Type Theory: Problems and Approaches - at TYPES 2015 with Thorsten Altenkirch and Paolo Capriotti
We discuss constructions that are desirable but cannot be performed in HoTT.
Eliminating Higher Truncations via Constancy - at TYPES 2014 with Paolo Capriotti
We generalize the universal property of n-truncations.
Isomorphism of Finitary Inductive Types - at TYPES 2014 with Christian Sattler
We present an algorithm for deciding isomorphism of finitary inductive types.
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.
The Truncation Map on Nat is Nearly Invertible (blog post) (Agda formalisation and explanation, html)
We construct a term which pretends to be an inverse of the truncation projection Nat -> ||Nat||.
1-Types and Set-Based Groupoids
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).
Non-Normalizability of Cauchy Sequences
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.
Some Families of Categories with Propositional Hom-Sets
A list defining complete partial orders, Heyting algebras and so on in terms of categories, to make up for my memory.
Setoids are not a LCCC
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.
Yoneda Groupoids
My Yoneda Groupoids are special weak omega groupoids that have a simple and short formalisation.
First Year Report, extended version
The shorter version of my report is an abridged version of the extended one. 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
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 my introduction focusses on models, which the book does not).
A direct proof of Hedberg's theorem in Coq, see also my post on the HoTT blog
A variant of the proof of Hedberg's theorem. Includes a slight improvement, namely "local decidability implies local UIP".
On String Rewriting Systems (draft)
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.
A Lambda Term Representation Inspired by Linear Ordered Logic [arXiv]
Together with Andreas Abel. Appeared at LFMTP 2011.