This section defines the interpretation of the syntax into the model. It is well known that to well define
an interpretation of judgements (rather than derivations) of dependent type theory
with the conversion rule, the syntax of the type theory must be
annotated with typing information. For example, Hofmann [1]} annotates the application term for \(\Pi \) 
types with the type of the function being applied, writing \(\mathsf {App}_{[x:A]B}(t,u)\)  rather than the more common
application term \(t\,u\) , in order to define an interpretation of syntax into a general CwF. Likewise lambda
expressions are annotated not just with the type of the variable being abstracted, but also with the target type
of the abstraction.
