20 citations · 33 across the 3 of their papers we have counts for
Showing 2019Show all
2 papers · 1 filter
cs.LO2019
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…
cs.LO2019★ 6 cited
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…