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
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?.
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.
2-type theory, 2-logic
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:
Daniel Licata, Dependently Typed Programming with Domain-Specific Logics PhD Thesis (2011) (pdf) - chapter 7
Dan Licata, Mike Shulman, Adjoint logic with a 2-category of modes, in Logical Foundations of Computer Science 2016 (pdf, slides)
Daniel Licata, Mike Shulman, and Mitchell Riley, A Fibrational Framework for Substructural and Modal Logics (extended version), in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (doi: 10.4230/LIPIcs.FSCD.2017.25, pdf)