41 citations · 172 across the 17 of their papers we have counts for
22 papers
Constructive Ordinal Exponentiation
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1
In classical mathematics, ordinal arithmetic is well-studied; constructively, addition and multiplication are well-known. We study constructive ordinal exponentiation, where ordina…
Set-Theoretic and Type-Theoretic Ordinals Coincide
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary…
Type-Theoretic Approaches to Ordinals
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate li…
A Rewriting Coherence Theorem with Applications in Homotopy Type Theory
Nicolai Kraus, Jakob von Raumer
Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to…
Connecting Constructive Notions of Ordinals in Homotopy Type Theory
Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and…
Internal -Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT
Nicolai Kraus
Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory…
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
Nicolai Kraus, Jakob von Raumer
Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not nec…
Shallow Embedding of Type Theory is Morally Correct
Ambrus Kaposi, András Kovács, Nicolai Kraus
There are multiple ways to formalise the metatheory of type theory. For some purposes, it is enough to consider specific models of a type theory, but sometimes it is necessary to r…
From Cubes to Twisted Cubes via Graph Morphisms in Type Theory
Gun Pinyo, Nicolai Kraus
Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent…
Path Spaces of Higher Inductive Types in Homotopy Type Theory
Nicolai Kraus, Jakob von Raumer
The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been deve…
Free Higher Groups in Homotopy Type Theory
Nicolai Kraus, Thorsten Altenkirch
Given a type A in homotopy type theory (HoTT), we can define the free infinity-group on A as the loop space of the suspension of A+1. Equivalently, this free higher group can be de…
Univalent Higher Categories via Complete Semi-Segal Types
Paolo Capriotti, Nicolai Kraus
Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent cat…
Two-Level Type Theory and Applications
Danil Annenkov, Paolo Capriotti, Nicolai Kraus +1
We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the inner and the outer type…
Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
Nicolai Kraus, Christian Sattler
Topologists are sometimes interested in space-valued diagrams over a given index category, but it is tricky to say what such a diagram even is if we look for a notion that is stabl…
Quotient inductive-inductive types
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra +2
Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotien…
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
Capretta's delay monad can be used to model partial computations, but it has the "wrong" notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay m…
Notions of Anonymous Existence in Martin-Löf Type Theory
Nicolai Kraus, Martín Escardó, Thierry Coquand +1
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedber…
Extending Homotopy Type Theory with Strict Equality
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to def…
Functions out of Higher Truncations
Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi
In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence…
The General Universal Property of the Propositional Truncation
Nicolai Kraus
In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, Sigma, Pi, and identity types), we define the type of constant…
Higher Homotopies in a Hierarchy of Univalent Universes
Nicolai Kraus, Christian Sattler
For Martin-Lof type theory with a hierarchy U(0): U(1): U(2): ... of univalent universes, we show that U(n) is not an n-type. Our construction also solves the problem of finding a…
A Lambda Term Representation Inspired by Linear Ordered Logic
Andreas Abel, Nicolai Kraus
We introduce a new nameless representation of lambda terms inspired by ordered logic. At a lambda abstraction, number and relative position of all occurrences of the bound variable…