Dependently typed algebraic theories

Dependently typed algebraic theories are a family of logical systems extending algebraic theories with dependent types , occasionally called dependent sorts. The prototypical example of a theory that should be, but is not technically, algebraic is the theory of categories. The problem is that the composition operation is partial when morphisms are viewed as a single type. Viewing the morphisms instead as a family of dependent types, parameterized by pairs of objects, composition becomes a family of total operations and the algebraic character of the theory is restored.

One of the earliest and best known notions of dependently typed algebraic theory is that of a generalized algebraic theory , introduced by John Cartmell along with their categorical semantics in contextual categories. Generalized algebraic theories are closely related to essentially algebraic theories and finite limit sketches, which have the same set-theoretic models. The late Vladimir Voevodsky revived interest in Cartmell’s contextual categories, which he re-axiomatized and dubbed C-systems, as part of the homotopy type theory project.

My original interest in dependently typed algebraic theories stems from the problem of designing a computer algebra system for category theory. Certain classic systems like Axiom and Maple are organized around algebraic theories, but algebraic theories are not expressive enough to define the theory of categories. The computer algebra system and programming library Catlab.jl is built around generalized algebraic theories.

Logical systems

Generalized algebraic theories (GATs)

  • Cartmell, 1986: Generalized algebraic theories and contextual categories (doi)
    • Defines generalized algebraic theories as a fragment of Martin-Lof type theory
    • GATs are interpreted in contextual categories
    • Based on Cartmell’s 1978 PhD thesis (pdf), which defines categories with attributes
  • Fiore, 2008: Second-order and dependently-sorted abstract syntax (doi, pdf)
    • Sec II gives “algebraic foundations” for dependent types in GATs, modeling contexts as presheaves in the style of Makkai
  • Garner, 2015: Combinatorial structure of type dependency (doi, arxiv)
    • Sec 2 summarizes the syntax of GATs and interpretations between GATs (equivalence classes of which are morphisms between GATs)
    • The “main task” of the paper is to “express the category GAT of generalized algebraic theories as the category of algebras for a monad on a presheaf category”
    • The presheaves (called in type-and-term structures in Def 8) are modeled on the linearly ordered concept of a context, unlike those in Fiore/Makkai
  • Sterling, 2019: Algebraic type theory and universe hierarchies (arxiv)

First-order logic with dependent sorts (FOLDS)

  • Makkai, 1995: First order logic with dependent sorts, with applications to category theory (pdf, abstract , nLab )
    • Readable, unpublished manuscript introducing FOLDS
    • Voevodsky: “Univalent Foundations can be seen as a realization of the vision of Michael Makkai whose paper (Makkai, 1995) was very important for me in my search for a formal language for contemporary Mathematics.” (doi)
    • See also Makkai’s philosophical works on categorical foundations
  • Boudreault, 2006, MSc thesis: Basic model theory of finitary and infinitary languages of first-order logic with dependent sorts (FOLDS) (pdf)
    • “We give here the exhaustive proofs for basic facts about the model theory of finitary and infinitary languages for FOLDS, most of which were sketched in (Makkai, 1995).”

Essentially algebraic theories

See also references on HoTT mailing list.

  • Freyd, 1972: Aspects of topoi (pdf)
    • Original source for definition of “essentially algebraic”
  • Adamek & Rosicky, 1994: Locally presentable and accessible categories, Section 3.D
  • Piessens & Steegmans, 1997: Proving semantical equivalence of data specifications (doi, pdf)
    • Application-oriented and mostly self-contained
    • Cited in Johnson et al, 2002: Entity-relationship-attribute designs and sketches (pdf), a precursor to Spivak’s work
  • Power & Wells, 1992: A formalism for the specification of essentially-algebraic structures in 2-categories (doi, pdf)
    • Shows that 2-categories are an essentially algebraic theory
    • Uses sketches for specification (e.g., sketch for Cat in Sec 6)
  • Porst, 1993: The algebraic theory of order (doi)
    • Exhibits the theory of partial orders as an essentially algebraic theory
  • Palmgren & Vickers, 2007: Partial Horn logic and cartesian categories (doi, pdf)
    • Introduces partial Horn logic (PHL) as an alternative syntax for essentially algebraic theories (equivalence proved in Sec 9)
    • Defines set-theoretic models of PHL based on partial maps (Sec 3)
    • Constructs a term model for a PHL theory (Sec 4) ala the term model for an algebraic theory
    • Uses notion of partial morphism in an arbitrary category (Sec 7) to define models in categories besides Set (Sec 8)
    • Constructs a syntactic category (classifying category) for a PHL theory (Sec 9)
    • Commentary: Sec 4 is easy, but everything in Sec 7-9 is very complicated compared to the simple construction of the syntactic category for an algebraic theory. The classifying category is constructed abstractly because the term model has no obvious categorical structure. After reading this paper I am far from persuaded that partiality is the right approach.
  • Isaev, 2017: Algebraic presentations of dependent type theories (arxiv)
    • Uses essentially algebraic theories (in form of PHL; see Palmgren & Vickers, 2007) to define a category of dependent type theories (“algebraic dependent type theories”)

Categorical semantics

Beginning with Cartmell’s categories with attributes and contextual categories, there has been a long and confusing line of work on different categorical models of dependent types , which includes Voevodsky’s work on C-systems.

  • Jacobs, 1993: Comprehension categories and the semantics of type dependency (doi, pdf)
    • Exposition of comprehension categories, which generalize contextual categories, categories with attributes, and categories with families
    • Further developed in the textbook (Jacobs, 1999: Categorical logic and type theory, Ch. 9 & 10)
  • Pitts, 1995: Categorical logic (pdf)
    • Exposits algebraic theories and generalized algebraic theories
    • Based on Cartmell’s work but uses type categories, which are nearly the same as categories with attributes
  • Hofmann, 1997: Syntax and semantics of dependent types (pdf)
    • Overview of dependent types (dependent sums, dependent products, etc)
    • Shows that categories with attributes are equivalent to categories with families
    • Published in two books, in slightly different forms:
      • Hofmann, 1997, PhD thesis: Extensional Constructs in Intensional Type Theory (doi)
      • Pitts & Dybjer, eds., 1997: Semantics and Logics of Computation (doi)
  • Newstead, 2021, PhD thesis: Algebraic models of dependent type theory (arxiv)
  • Zhang, 2021, expository notes: Type theories in category theory (arxiv)