nLab
type formation

Idea

In type theory a type formation rule is a natural deduction step roughly of the form

$$\frac{⊢A:\mathrm{Type}⊢B:\mathrm{Type}\cdots }{⊢F(A,B,\cdots ):\mathrm{Type}}$$\frac{ \vdash\; A \colon Type \;\;\; \vdash \;B \colon Type \;\;\; \cdots }{ \vdash \; F(A,B,\cdots) \colon Type }

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

$$\frac{⊢A:\mathrm{Type}⊢B:\mathrm{Type}}{⊢A\times B:\mathrm{Type}}.$$\frac{\vdash \; A \colon Type \;\;\; \vdash \; B \colon Type}{\vdash \; A \times B \colon Type} \,.

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:

1. type formation rule

2. term introduction rule

3. term elimination rule

4. computation rule

Properties

Relation to category theory

Under the relation between type theory and category theory, the categorical semantics of type formation essentially corresponds to certain universal constructions in category theory.