# 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

On 2-type theory:

• R.A.G. Seely, Modeling computations: a 2-categorical framework, LICS 1987 (pdf)

• Richard Garner, Two-dimensional models of type theory, Mathematical structures in computer science 19.4 (2009): 687-736 (doi:10.1017/S0960129509007646, pdf)

• Tom Hirschowitz, Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (3), pp.10. (pdf)

• Philip Saville, Cartesian closed bicategories: type theory and coherence. PhD thesis, 2020. pdf.

Application to adjoint logic and modal type theory: