41 citations · 172 across the 17 of their papers we have counts for
16 papers · 1 filter
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…
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…
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…
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…
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…
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…