nLab synthetic (infinity,1)-category theory

Idea

In general, by synthetic $(\infty,1)$-category theory one will want to mean some formulation of (∞,1)-category theory in the spirit of synthetic mathematics, here specifically relating to synthetic homotopy theory as $\infty$-category theory relates to homotopy theory.

One implementation of this idea was proposed by Riehl & Shulman 2017, based on a variant of homotopy type theory called simplicial type theory. This is further developed by Buchholtz & Weinberger 2021.

Another implementation of this idea was proposed by Weaver & Licata 2020.

See also

• internal category in homotopy type theory

• synthetic mathematics, synthetic homotopy theory

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

• directed homotopy type theory

• simplicial type theory, cubical type theory

References

For synthetic (infinity, 1)-category theory in cubical type theory:

• Matthew Weaver, Daniel Licata. “A Constructive Model of Directed Univalence in Bicubical Sets”. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’20. Saarbrücken, Germany: Association for Computing Machinery, 2020, pp. 915–928. (doi:10.1145/3373718.3394794)

For synthetic (infinity, 1)-category theory in simplicial type theory:

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

• Ulrik Buchholtz, Jonathan Weinberger, Synthetic fibered $(\infty,1)$-category theory $[$arXiv:2105.01724, talk slides$]$

• Jonathan Weinberger, A Synthetic Perspective on $(\infty,1)$-Category Theory: Fibrational and Semantic Aspects $[$arXiv:2202.13132$]$

• Fredrik Bakke, Segal Spaces in Homotopy Type Theory. Master thesis $[$no.ntnu:inspera:99217069:14871483$]$

• César Bardomiano Martínez, Limits and colimits of synthetic $\infty$-categories $[$arXiv:2202.12386$]$

• Jonathan Weinberger, Strict stability of extension types $[$arXiv:2203.07194$]$

• Jonathan Weinberger, Two-sided cartesian fibrations of synthetic $(\infty,1)$-categories $[$arXiv:2204.00938$]$

• Jonathan Weinberger, Internal sums for synthetic fibered $(\infty,1)$-categories $[$arXiv:2205.00386$]$

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)