Skip to main content
Source Link

An important example from type theory/categorical logic: the forgetful functor from categories with families (or variants) to categories with attributes (or variants).

Briefly, both are category-based structures encoding the structure of a dependent type theory (and hence the structure needed to interpret such a theory). A category with families consists of a category of contexts, a presheaf of types over contexts, and a further presheaf of terms indexed over types, together with an operation of context extension satisfying a certain universal property.

The universal property forces terms to correspond to sections of certain projection maps. Categories with attributes take advantage of that, including just the category of contexts, the presheaf of types, the extension operation, and the projection maps.

So the forgetful functor is indeed an equivalence, and genuinely not an isomorphism: Given a CwF, if you forget to the underlying CwA, you can recover original the presheaf of terms just up to isomorphism.

Each notion has some advantages. CwA’s are a little “tighter” and easier to set up, since they involve less data; but taking the preheaf of terms as primary, in CwF’s, simplifies some later constructions, and allows very fruitful analyses and generalisations.

Post Made Community Wiki by Peter LeFanu Lumsdaine