Generalized algebraic theories and contextual categories (Q1096716): Difference between revisions

The author presents a `doctrine' of functorial semantics which, as far as usual set-theoretic models are concerned, has the same descriptive power as Freyds's ``essentially algebraic theories'' [cf. \textit{P. Freyd}, Bull. Austral. Math. Soc. 7, 1-76, 467-480 (1972; Zbl 0252.18001 and Zbl 0252.18002)]. So, for instance, the notion of `category' can be described in it. However, whereas for instance the Freyd description of the notion of category depends on comprehending the totality of arrows of a category into one set, Cartmell's notions have direct notation and semantics for families of sets (like: the family of hom sets of a category), namely variable types a la Martin-Löf. (It would appear, therefore, that also the notion of V-enriched category is describable, uniformly in V, in Cartmell's doctrine.) The paper provides most of what one asks for in connection with a doctrine: a syntax, a categorical notion of `theory' (here: a ``contextual'' category, which is a category with a fair amount of extra structure); and a basic large contextual category for the semantics (here, the contextual category Fam of ``families of... families of sets''.