natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
In type theory a type formation rule is a natural deduction step roughly of the form
which says that given types $A, B, \cdots$, there is a new type $F(A,B, \cdots)$.
For instance for product types it says that
In natural deduction the type formation rule for a kind of type in the first in a quadruple of rules that come with every kind of type:
type formation rule
Under the relation between type theory and category theory, the categorical semantics of type formation essentially corresponds to certain universal constructions in category theory.