20 citations · 27 across the 2 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2020★ 7 cited
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.…
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…