Comment by TimorousBestie
5 hours ago
> I am interested in different approach to types, using triage calculus, which is more "materialist" than "structuralist" - type is given by the structure of the (quoted) term in normal form (unlike lambda calculus, triage calculus makes quoting easy).
Interesting, dropping this link here for others: https://treecalcul.us/
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.