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
Formal -category theory is to -category theory what formal category theory is to 1-category theory, that is: a synthetic approach to -categories standing in relation to synthetic homotopy theory as -category theory stands to homotopy theory. Consequently, formal -category theory has also been called synthetic -category theory.
There have been two main styles of approaches to formal -category theory: categorical, which are -categorical in nature; and type theoretic, which propose deductive systems for reasoning about -categories.
Following Joyal 2008 p. 158, Riehl & Verity 2013 observe that the homotopy 2-category of -categories retains much of the interesting structure of the -category . Thus, one may use the techniques of formal category theory to study certain aspects of the formal theory of -categories. For instance, this includes the theory of adjoint -functors (which are automatically homotopy coherent), but not the theory of -monads (which are not). This is developed in Elements of ∞-Category Theory in the setting of a virtual equipment.
For presentable -categories, formal -category theory is directly accessible from “abstract homotopy theory” in the sense of combinatorial model category-theory, in that 2Ho(CombModCat) (Pavlov 2021).
Ruit 2023 has introduced an -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 -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 October 14, 2023 at 06:21:06. See the history of this page for a list of all contributions to it.