nLab simplicial type theory

Idea

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.

See also

• Reedy model structure

• bisimplicial set

• synthetic $(\infty,1)$-category theory

• type theory with shapes

• two-level type theory

References

• Emily Riehl, Michael Shulman, A type theory for synthetic $\infty$-categories $[$arXiv:1705.07442$]$

• Jonathan Weinberger, A Synthetic Perspective on $(\infty,1)$-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?:

• Emily Riehl, The synthetic theory of infinity-categories vs the synthetic theory of infinity-categories, Homotopy Type Theory Electronic Seminar Talks, 1 March 2018, (video, slides)

A proof assistant implementing simplicial type theory:

• rzk