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
Formal $(\infty,1)$-category theory is to $(\infty,1)$-category theory what formal category theory is to 1-category theory, that is: a synthetic approach to $(\infty,1)$-categories standing in relation to synthetic homotopy theory as $(\infty, 1)$-category theory stands to homotopy theory. Consequently, formal $(\infty,1)$-category theory has also been called synthetic $(\infty,1)$-category theory.
There have been two main styles of approaches to formal $(\infty,1)$-category theory: categorical, which are $(\infty,2)$-categorical in nature; and type theoretic, which propose deductive systems for reasoning about $(\infty,1)$-categories.
Following Joyal 2008 p. 158, Riehl & Verity 2013 observe that the homotopy 2-category of $(\infty,1)$-categories $2Ho\big( Cat_{(\infty,1)}\big)$ retains much of the interesting structure of the $(\infty,2)$-category $Cat_{(\infty,1)}$. Thus, one may use the techniques of formal category theory to study certain aspects of the formal theory of $(\infty,1)$-categories. For instance, this includes the theory of adjoint $(\infty,1)$-functors (which are automatically homotopy coherent), but not the theory of $(\infty,1)$-monads (which are not). This is developed in Elements of ∞-Category Theory in the setting of a virtual equipment.
For presentable $(\infty,1)$-categories, formal $(\infty,1)$-category theory is directly accessible from “abstract homotopy theory” in the sense of combinatorial model category-theory, in that $2Ho\big( PresCat_{(\infty,1)}\big) \,\simeq\,$ 2Ho(CombModCat) (Pavlov 2021).
Ruit 2023 has introduced an $\infty$-double categorical generalisation of fibrant double categories.
Riehl & Shulman 2017 propose a type theory called simplicial type theory, which have categorical semantics in bisimplicial sets. This is further developed by Buchholtz & Weinberger 2021.
Weaver & Licata 2020 propose a type theory, with semantics in bicubical sets.
With (small) (∞,1)-categories modeled as quasi-categories, their homotopy 2-category was considered first in
and then developed further (in the generality of homotopy 2-categories of ∞-cosmoi) in:
Emily Riehl, Dominic Verity, The 2-category theory of quasi-categories, Advances in Mathematics Volume 280, 6 August 2015, Pages 549-642 (arXiv:1306.5144, doi:10.1016/j.aim.2015.04.021)
Emily Riehl, Dominic Verity, Infinity category theory from scratch, Higher Structures Vol 4, No 1 (2020) (arXiv:1608.05314, pdf)
Emily Riehl, Dominic Verity, Elements of ∞-Category Theory, Cambridge studies in advanced mathematics 194, Cambridge University Press (2022) $[$doi:10.1017/9781108936880, ISBN:978-1-108-83798-9, pdf$]$
Emily Riehl, The formal theory of ∞-categories, talk at Categories and Companions Symposium June 8–12, 2021 (video)
In an (∞,1)-category theoretic version of proarrow equipments:
For synthetic (infinity, 1)-category theory in cubical type theory via bicubical sets:
Exposition in
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:
Last revised on October 14, 2023 at 06:21:06. See the history of this page for a list of all contributions to it.