Nicolai Kraus

I am a PhD student of Thorsten Altenkirch at the Functional Programming Laboratory (School of Computer Science, University of Nottingham). My main interests are Homotopy Type Theory and related subjects.

Feel free to contact me: ngk at cs.nott.ac.uk

Some of my work (in reversed chronological order)

Any comments are highly appreciated.

Main work

The Universe U_n is not an n-type [pdf][formalized proof][HoTT blog post]

With Christian Sattler.
In basic MLTT with the univalence axiom, it is well-known that the universe U is not a set (i.e. does not have unique identity proofs). It is plausible to expect that the next universe in the hierarchy, i.e. U_1, is not a groupoid, but showing this is surprisingly difficult. We generalize the statement and show that the universe U_n is not an n-type. At the same time, our construction yields a type that is an (n+1)-type but not an n-type. This answers one of the questions asked at the UF Program in Princeton.

Generalizations of Hedberg’s Theorem [ pdf preprint][Agda file][HoTT blog post]

With Martin Escardo, Thierry Coquand and Thorsten Altenkirch. To appear at TLCA 2013.
Hedberg's Theorem states that a type with decidable equality has unique identity proofs. This statement is strengthened in several ways. The blog post only contains a small part of the contents, while the Agda file includes additional thoughts. The final publication will be available at link.springer.com.

Talks

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. Contains generalizations of the theorem, 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.

Other Drafts, Notes, Miscellaneous Contents

Everything that is marked as "draft" is fairly incomplete. The converse is not necessarily true.

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

Notes on Yoneda Groupoids, the Construction of their Higher Quotients, and the Root of Equality (draft)

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

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.

A direct proof of Hedberg's theorem in Coq, see also my post on the HoTT blog

Hedberg's theorem states that decidability of equality implies UIP. Reading through the original proof, I noticed that this can be done more directly, using that "decidable equality" looks literally similar to "contractible". There is also a slight improvement, namely "local decidability implies local UIP".

On String Rewriting Systems (draft)

Unfinished draft, joint work with Christian Sattler. We define a translation for non-confluent String Rewriting Systems systems, enabling us to normalize derivation sequences to some extent.

Homotopy Type Theory - An overview

My introduction to HoTT (also the main part of my first year report).

A Lambda Term Representation Inspired by Linear Ordered Logic

Together with Andreas Abel. Appeared at LFMTP 2011, DOI: 10.4204/EPTCS.71.1