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 (or should be) for directed homotopy theory/(∞,n)-category theory.
One candidate for full omega-categories i.e. (∞,∞)-categories is opetopic type 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)
Dan Licata, Chapters 7 and 8 of Dependently Typed Programming with Domain-Specific Logics PhD thesis, (pdf)
Andreas Nuyts?, Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance, PDF
Emily Riehl and Mike Shulman, A type theory for synthetic ∞-categories, Higher Structures, 2017, arxiv
Paige Randall North, Towards a directed homotopy type theory, (arXiv:1807.10566)
Last revised on June 18, 2020 at 14:43:13. See the history of this page for a list of all contributions to it.