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…