The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I'm working on Coqing category theory, and found that I needed the same construction/proofs for comma categories and for (op)lax slice categories, and thought that I'd get a better logical separation of code if I generalized [sigT] to categories.  I have mostly done this (code available, for now, at https://dl.dropbox.com/u/11313181/Temp/sigCat.zip and https://dl.dropbox.com/u/11313181/Temp/sigCat/sigCategory.v, if anyone wants to see what I've done so my questions make more sense).  I defined a category where objects and morphisms are each a sigma type of the original morphisms and objects of the category.  I "discovered" that [sig] corresponds to full subcategories, wide subcategories, and subcategories when done on the objects, morphisms, and both, respectively.  The product category, and the projection functors, correspond to [prod], [fst] and [snd], which I know are the non-dependent versions of [sigT].  Do dependently typed sigma categories exist anywhere in the literature?  Wikipedia (http://en.wikipedia.org/wiki/Intuitionistic_type_theory#Categorical_models_of_type_theory) suggests that they might be "categories with families", though I don't really understand the correspondence in that part.  I've defined the functor analogue of [projT1], but I am stumped on the analogue of [projT2].  Does it exist?  (Does it exist with my formulation of [sigT] categories, or only more specific/general ones?)

Thanks.

-Jason