Nicolai Kraus
University of Nottingham, School of Computer Science, Office A06
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 General Universal Property of the Propositional Truncation [pdf]

The universal property of the propositional truncation says that the types A > B and A > B are equivalent if B is propositional. I consider the case that B is not necessarily propositional, but only an ntype for some fixed n, or not known to be truncated at all. Assuming a type theory with Reedy omegalimits, I define a type of constant functions A > B which satisfy an infinite tower of coherence conditions. I then show that this type is homotopy equivalent to the type A > B without any conditions on B. If B is an ntype, the equivalence can be stated and proved in "standard HoTT" (without the assumption of nontrivial Reedy limits).

Notions of Anonymous Existencs in MartinLöf Type Theory [pdf preprint][formalization (html)][formalization (source, zip)]

With Martin Escardo, Thierry Coquand and Thorsten Altenkirch. Contribution to the special issue of TLCA 2013.
We discuss weakly constant functions, in particular endofunctions, and different related notions of existence.

On the Hierarchy of Univalent Universes: U(n) is not nTruncated
[article]
[formalization (html)]
[formalization (source)]
[blog post]

With Christian Sattler.
We show that, assuming a hierarchy U(0), U(1), U(2), ... of univalent universes, the universe U(n) is not ntruncated (without using HITs). Further, if we restrict U(n) to ntypes, it is a "strict" n+1type. We also define a notion of nconnectedness that does not make use of HITs and show how to construct the nconnected version of a type.

Generalizations of Hedbergâ€™s Theorem [pdf preprint][formalization (html)][HoTT blog post]

With Martin Escardo, Thierry Coquand and Thorsten Altenkirch. 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 is available at
link.springer.com.
Some Talks (for which I have slides  I actually prefer blackboards)

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 Eidhoven, 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. 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

Eliminating Higher Truncations via Constancy  at TYPES 2014 with Paolo Capriotti

We generalize the universal property of ntruncations.

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 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 formalization and explanation)

We construct a term which pretends to be an inverse of the truncation projection Nat > Nat.

1Types and SetBased Groupoids

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

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

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

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 nonconfluent String Rewriting Systems systems, enabling us to normalize derivation sequences to some extent.
We had developed the described techniques in order to tackle a famous problem on onerule string rewriting systems (see the RTA open problems list).

A Lambda Term Representation Inspired by Linear
Ordered Logic

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