Dependently typed algebraic theories

• 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)
  • Part II gives “algebraic foundations” (abstract syntax) 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)

• 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).”

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”)