8 papers
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…