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
Simplicial type theory (Riehl & Shulman 2017, §3) is a homotopy type theory which introduces additional non-fibrant layers on top of Martin-Löf type theory to provide a logical calculus for a directed interval type and with it for geometric shapes, consisting of cube judgments, tope judgments, inequality topes, extension types, Segal space-types, Rezk complete-types, and covariant fibrations.
Emily Riehl, Mike Shulman, A type theory for synthetic ∞-categories, Higher Structures 1 1 (2017) [arxiv:1705.07442, published article]
Jonathan Weinberger, A Synthetic Perspective on -Category Theory: Fibrational and Semantic Aspects arXiv:2202.13132
Jonathan Weinberger, Strict stability of extension types arXiv:2203.07194
A talk on synthetic (infinity,1)-category theory in simplicial type theory and infinity-cosmos theory:
A proof assistant implementing simplicial type theory:
Last revised on March 6, 2023 at 08:17:19. See the history of this page for a list of all contributions to it.