nLab directed type theory

Any kind of type theory with categorical semantics in 2-categories or (n,2)-categories, such as $(\infty,2)$-categories. See:

• 2-type theory

• directed homotopy type theory

category: disambiguation