69 citations · 219 across the 12 of their papers we have counts for
13 papers
The Groupoid-Syntax of Type Theory is a Set
Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the t…
Internal parametricity, without an interval
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi +1
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usua…
Should Type Theory replace Set Theory as the Foundation of Mathematics
Thorsten Altenkirch
We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory.
The Integers as a Higher Inductive Type
Thorsten Altenkirch, Luis Scoccola
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its ind…
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…
Normalisation by Evaluation for Type Theory, in Type Theory
Thorsten Altenkirch, Ambrus Kaposi
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient indu…