1
$\begingroup$

In "Syntax and Semantics of Dependent Types" at the top of page 24, Martin Hoffman describes $\mathit{Ty}_{\mathcal C}(\Gamma)$ as the collection of semantic types under context $\Gamma$.

It makes sense that he used the word collection rather than set, because in the set-theoretic CwF he describes, the types under a context $\Gamma$ are $\Gamma$-indexed families of sets. It is well known that this is a proper class.

However, on page 26 he provides a more abstract definition where a CwF is a Fam-valued presheaf. Such a presheaf maps an object $\Gamma$ of the context category onto a pair (Ty($\Gamma$), $\mathit{Tm}(\Gamma,\sigma)_{\sigma \in \mathit{Ty}(X)}$). The left component of an object of Fam is an index set, so this contradicts the earlier definition and seems incorrect. Most literature on CwF's takes the same approach. Would it be more appropriate to use the category of class-indexed families of sets as the codomain category for these presheaves?

$\endgroup$
2
$\begingroup$

There is nothing special about types with respect to sizing, compared to what we already have in ordinary categories. A small category has a set of objects, and for each pair of objects, a set of morphisms between them; so morphisms are an indexed family of sets. We can immediately extend this definition to small CwFs, where for each context we have a set of types.

All that happens, compared to categories, is that we have four underlying set families (objects, morphisms, types, terms) instead of just objects and morphisms, so we have more degree of freedom when choosing the sizes involved. E.g. we have locally small categories where the set of objects is large (in some sense) and the sets of morphisms are small, and we're likewise free to pick relative sizes of all involved sets in CwFs.

$\endgroup$
2
  • $\begingroup$ Thank you for the answer. I don't think I've considered that ordinary categories can be viewed as indexed families of hom-sets before. $\endgroup$ Nov 26 at 16:13
  • $\begingroup$ Okay, I think I understand what the issue is. I was using the set-theoretic definition of "set" rather than the category-theoretic one (i.e. a discrete category). Using the category-theoretic definition, Fam does not necessarily have a small set of objects. $\endgroup$ Nov 26 at 16:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.