On Mon, Mar 05, 2018 at 01:29:56PM -0800, Michael Shulman wrote:
> By a standard construction (described for example at
> https://ncatlab.org/nlab/show/categorical+model+of+dependent+types),
> categories with families are equivalent to categories with attributes,
> i.e. to comprehension categories that are discrete fibrations.

On Wed, Mar 7, 2018 at 6:09 PM, Thomas Streicher <stre...@mathematik.tu-darmstadt.de> wrote:

 

That's misleading I think. One rather should think categories with
attributes as full comprehension categories

- (1) The axioms for CwA’s themselves, and for logical structure on them, involve *lots* of on-the-nose equalities between types over a given context.  This is perfectly natural when they’re seen as discrete comp cats (since then on-the-nose equality is the same as isomorphism in the fibre); seen as full split ones, it violates the principle of equivalence (i.e. respecting isomorphisms).

- (2) The treatment of logical structure becomes more uniform between comp cats and CwA’s under the “discrete” viewpoint.  In the Lumsdaine–Warren “Local Universes…” paper (https://arxiv.org/abs/1411.1736), where we followed the established “full split” view, we had to define two separate versions of each piece of logical structure: “strictly stable” structure as the natural notion for CwA’s, and “pseudo-stable” structure as the natural notion for comprehension cats.  With the discrete viewpoint, these are a single notion: pseudo-stable structure on a discrete comp cat gives exactly strictly stable structure!

- (3) 2-categorically, the picture is much nicer under the “discrete” view.  This is a bit too much to fully describe in a quick email, but one manifestation is the fact that viewing CwA’s as discrete comprehension categories, one gets natural inclusion 2-functors

CxlCat —> CwA —> CompCat

which are each 2-full-and-faithful, i.e. induce equivalences on hom-categories.  Here CxlCat is the usual 1-category, viewed as a locally discrete 2-category; CwA is a fairly natural 2-category of CwA’s (Voevodsky convinced me that this is much more natural than the 1-category of CwA’s more usually considered); and CompCat is a 2-category in the “obvious” way.

A “toy model” of the issues involved: you can embed Set into Cat as either the discrete or the codiscrete categories.  Viewed 1-categorically, both of these are perfectly nice full and faithful functors; but 2-categorically, while the “discrete” embedding is 2-full-and-faithful, the codiscrete embedding is *very* far from being so. And this can be seen as lying behind the various ways in which the “discrete” embedding Set —> Cat is more natural for almost all purposes.

Going back to CwA’s/comp cats: the one big *advantage* I see of the “full split” embedding is for the categorical analysis of type-constructors — e.g. the analysis of Pi-types and Sigma-types as adjoints — since the constructions are on types, but their universal properties involve general context morphisms.  This I agree is much cleaner under the “full split” view.  On the other hand, it’s not lost in the “discrete” view — e.g. it can be seen as a statement that these constructors become adjoints after applying “fullification” to the discrete comp cat in question.

–p.