Comment by js8

Yes. In type theory, the term carrying a type is a metalogical notion. In triage calculus, you can define a typechecking program that operates on a quoted term and normalizes only if the term typechecks.

This means in triage calculus (unlike in lambda calculus, which lacks means to quote programs) you can include expected input data types in your programs.

You can also construct any type theory syntactically by putting together a set of terms in triage calculus which only normalize when composed with correct types.

In triage calculus, you can then study types and propositions as any other programs - using self-interpretation. But I believe, as I detail below, a univalence principle is needed, to postulate the equivalence of metalogical triage calculus and its representation within triage calculus.