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.
Last revised on July 7, 2020 at 21:43:25. See the history of this page for a list of all contributions to it.