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.
2-type theory, 2-logic
2-categorical type theory is discussed in chapter 7 of
A more encompassing discussion of 2-categorical logic is being developed at