Background
Basic concepts
equivalences in/of $(\infty,1)$-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 $(\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.
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$]$
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$]$
Last revised on June 21, 2022 at 01:22:41. See the history of this page for a list of all contributions to it.