The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

You might also be interested in work on 2-dimensional type theory, in
which types represent categories (or more generally objects of some
2-category) and thus Sigma-types are Sigma-categories.  See for
instance
http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf

Mike

On Sun, Aug 5, 2012 at 5:34 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> 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