5 papers
Extension Types for Free
Nicolai Kraus
Extension types are a concept in dependent type theory that has appeared in various contexts. The idea is to have types whose terms are partially determined, e.g. via a strict boun…
Generalized Decidability via Brouwer Trees
Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh +1
In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable…
The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
Tom de Jong, Nicolai Kraus, Axel Ljungström
Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can…
A study of Kock's fat Delta
Tom de Jong, Nicolai Kraus, Simona Paoli +1
Motivated by the study of weak identity structures in higher category theory we explore the fat Delta category, a modification of the simplex category introduced by J. Kock and pro…
On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus +1
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form . The case of the circle has a slick answer: th…