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
What homotopy type theory is for homotopy theory/(∞,1)-category theory, directed homotopy type theory is for directed homotopy theory/(∞,n)-category theory.
Robert Harper, Dan Licata, Canonicity for 2-Dimensional Type Theory (pdf)
Robert Harper, Dan Licata, 2-Dimensional directed dependent type theory (pdf slides)
Michael Warren, Directed Type Theory (video lecture)
Also chapters 7 and 8 of