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 is 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.
Introductory textbook account:
Last revised on November 3, 2022 at 16:20:52. See the history of this page for a list of all contributions to it.