Function types

Given types and , the function type contains mappings whose inputs are in and outputs are in , i.e. functions. Under propositions as types, this corresponds to implication, since a term of takes proofs of to proofs of .

Standard presentation

In the cartesian calculus of substitutions we can introduce function types with the following typing rules. The formation, introduction, and elimination rules are

while we also have the substitution naturality rules

and judgemental computation rules for β-computation and η-unicity

From -types

In the Cartesian calculus of substitutions with -types, it is not necessary to give separate typing rules to establish function types. Instead we have

and so we can define .

Derivation of above typing rules

For we have

so we take .

For we have

so we take .

The derivations of , , , , and follow directly from those of the -type taking into account the equalities

which follow from .

#state/develop | #lang/en | #SemBr