Categorical Logic and Type Theory

By Bart P. F. Jacobs. Studies in Logic and the Foundations of Mathematics, 2001

771 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/c1e616595da3d0f08455024884d918bed7f3620a

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

Citations in the corpus

A type theory for synthetic ∞-categories (2017, background): “12 The dependency between levels is encoded with fibrations as in [7].”
Types are weak ω‐groupoids (2008, neutral): “For a more detailed treatment we refer the reader to [12, 18], for example.”
Types and programming languages: the next generation (2003, background): “Foundations for the semantics of types in the mathematical framework of category theory can also be found in many sources, including the books by Jacobs (1999), Asperti and Longo (1991), and Crole (1994); a brief primer can be found in Basic Category Theory for Computer Scientists (Pierce, 1991a).”
Double Categories of Relations (2021, positive): “A shorter proof of Theorem 9.4 might simply quote the criteria of Theorem 4.4.4 in [Jacobs, 1999].”
Fibred 2-categories and bicategories (2012, methodology): “tion in categorical logic: in describing comprehension schema for categories [Gra69, Law70] and via indexed categories [PS78]. For an overview of applications to categorical logic and type theory see [Jac99]. Fibrations were also used by Benabou [B´en85] to describe some foundations of category theo”
Elementary quotient completion (2012, positive): “That approach proved extremely fruitful, see (Makkai and Reyes 1977; Lambek and Scott 1986; Jacobs 1999; Taylor 1999; van Oosten 2008) and the references therein.”
Cubical sets and their site (2003, positive): “The exposition is modelled on the case of algebraic theories in cartesian categories [9, 20 , 25] with the necessary generalisations; some of the ideas behind the analysis can be found in [2] and [21].”
A framework for typed HOAS and semantics (2003, background): “[11]).”
Familial 2-functors and parametric right adjoints (2007, positive): “Indeed the fibration Fam(X)→Set which takes a family of objects to its indexing set is one of the guiding examples for the use of fibrations to organise logic and type theory [6] [18].”