21 citations · 58 across the 8 of their papers we have counts for
11 papers
For Generalised Algebraic Theories, Two Sorts Are Enough
Samy Avrillon, Ambrus Kaposi, Ambroise Lafont +2
Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. For example, the theories of categories or Martin-L{ö}f type theories form GATs. Categories have…
Type Theory with Single Substitutions
Ambrus Kaposi, Szumi Xie
Type theory can be described as a generalised algebraic theory. This automatically gives a notion of model and the existence of the syntax as the initial model, which is a quotient…
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…
For the Metatheory of Type Theory, Internal Sconing Is Enough
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global…
Relative induction principles for type theories
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a func…
Large and Infinitary Quotient Inductive-Inductive Types
András Kovács, Ambrus Kaposi
Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors.…
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…
Signatures and Induction Principles for Higher Inductive-Inductive Types
Ambrus Kaposi, András Kovács
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts…
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…
Free Applicative Functors
Paolo Capriotti, Ambrus Kaposi
Applicative functors are a generalisation of monads. Both allow the expression of effectful computations into an otherwise pure language, like Haskell. Applicative functors are to…