3

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 ...


Only top voted, non community-wiki answers of a minimum length are eligible