  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 refer to the syntax, for example in proofs of
canonicity and normalisation. One option is to embed the syntax deeply, by
using inductive definitions in a proof assistant. However, in this case the
handling of definitional equalities becomes technically challenging.
Alternatively, we can reuse conversion checking in the metatheory by shallowly
embedding the object theory. In this paper, we consider the standard model of a
type theoretic object theory in Agda. This model has the property that all of
its equalities hold definitionally, and we can use it as a shallow embedding by
building expressions from the components of this model. However, if we are to
reason soundly about the syntax with this setup, we must ensure that
distinguishable syntactic constructs do not become provably equal when
shallowly embedded. First, we prove that shallow embedding is injective up to
definitional equality, by modelling the embedding as a syntactic translation
targeting the metatheory. Second, we use an implementation hiding trick to
disallow illegal propositional equality proofs and constructions which do not
come from the syntax. We showcase our technique with very short formalisations
of canonicity and parametricity for Martin-L\"of type theory. Our technique
only requires features which are available in all major proof assistants based
on dependent type theory.
