Contents

# Contents

## Idea

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

$\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{\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 is 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.

Last revised on July 7, 2020 at 21:43:25. See the history of this page for a list of all contributions to it.