Contents

Contents

Idea

As type theory has categorical semantics in 1-categories, 2-type theory has semantics in 2-categories. There are, potentially, many different kinds of “2-type theory” with different uses and semantics. 2-type theory is closely related to (and sometimes the same as) directed type theory?.

Applications

• The “mode theories” in some general approaches to modal type theory and adjoint type theory are a form of 2-type theory, where the 2-cells represent a general form of “structural rules” acting on modal judgments.

• The 2-cells in 2-type theory can also be used to model rewriting, e.g. the process of $\beta$-reduction.

References

Last revised on December 7, 2018 at 02:29:49. See the history of this page for a list of all contributions to it.