Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
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
In general, by synthetic -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 -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.
For synthetic (infinity, 1)-category theory in cubical type theory:
For synthetic (infinity, 1)-category theory in simplicial type theory:
Emily Riehl, Michael Shulman, A type theory for synthetic -categories arXiv:1705.07442
Ulrik Buchholtz, Jonathan Weinberger, Synthetic fibered -category theory arXiv:2105.01724, talk slides
Jonathan Weinberger, A Synthetic Perspective on -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 -categories arXiv:2202.12386
Jonathan Weinberger, Strict stability of extension types arXiv:2203.07194
Jonathan Weinberger, Two-sided cartesian fibrations of synthetic -categories arXiv:2204.00938
Jonathan Weinberger, Internal sums for synthetic fibered -categories arXiv:2205.00386
A talk on synthetic (infinity,1)-category theory in simplicial type theory and infinity-cosmos theory:
Last revised on May 20, 2023 at 03:41:59. See the history of this page for a list of all contributions to it.