Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: indexed categories as dependent types

Matteo Capucci (he/him) (Feb 17 2021 at 18:24):

This is almost a reference request, but how true is the fact that 'indexed categories' are categories defined over a dependent type in the internal type theory of $Cat$? Or do I get double indexed categories?

Fawzi Hreiki (Feb 17 2021 at 19:22):

Well a hyperdoctrine is just an indexed category with quantifiers no?

Fawzi Hreiki (Feb 17 2021 at 19:23):

Bart Jacobs' book 'Categorical Logic and Type Theory' takes the fibred category approach to this.

Mike Shulman (Feb 18 2021 at 01:40):

I'm not sure what "defined over a dependent type" means. Inside of a 2-category such as Cat, you can define fibrations, and a C-indexed category is equivalent to a fibration over C. Of course an internal category in Cat would be a double category, and an internal category in the 2-category of fibrations over C would be a double indexed category.

Mike Shulman (Feb 18 2021 at 01:40):

Regarding indexed categories in internal type theories, you might be interested in these slides.

Matteo Capucci (he/him) (Feb 18 2021 at 09:40):

Mike Shulman said:

I'm not sure what "defined over a dependent type" means.

Right, it's not very clear. In my head it corresponds to give the definition of category in the TT but every context has some $c : C$ in it. I don't know if it's a sensible thing to do.
Explicitly, you give the definitione like this: a 'category indexed by $C$' is a type of objects $c : C \vdash O\,c$ together with a type of morphisms $c : C, o,o' : O\,c \vdash M\,c\,o\,o'$, a composition $c : C, o,o',o'' : O\,c \vdash (M\,c\,o\,o') \times (M\,c\,o'\,o'') \to (M\,c\,o\,o'')$ and an identity $c : C, o : O\,c \vdash 1_o : M\,c\,o\,o$ such that some equations hold

Joe Moeller (Feb 18 2021 at 14:11):

Mike Shulman said:

I'm not sure what "defined over a dependent type" means. Inside of a 2-category such as Cat, you can define fibrations, and a C-indexed category is equivalent to a fibration over C. Of course an internal category in Cat would be a double category, and an internal category in the 2-category of fibrations over C would be a double indexed category.

I'm going to guess that categories internal to $\mathsf{Fib}(C)$ are equivalent to pseudofunctors $C \to \mathsf{Dbl}$, categories internal to $\mathsf{Fib}$ are equivalent to double functors $D \to \mathsf{Cat}$, and that these are equivalent to each other when the base category has finite limits. I haven't checked it at all though.

Mike Shulman (Feb 18 2021 at 15:32):

Matteo Capucci (he/him) said:

In my head it corresponds to give the definition of category in the TT but every context has some $c : C$ in it.

Sure, that's just a category in context $C$, or equivalently a function from $C$ to the type $\mathsf{Cat}$ of categories. If it's interpreted in the internal logic of Set, you get literally a set $C$ and a $C$-indexed family of categories. To interpret it in the "internal logic of Cat", you have to say what you mean by the latter: are the dependent types arbitrary categories over categories? Fibrations? Opfibrations? If they're fibrations, then just a simple dependent type $c:C \vdash D\,\mathsf{type}$ is already (equivalent to) an indexed category, and a $C$-indexed family of categories as you describe is a category internal to indexed categories, i.e. an indexed double category. One thing you can say, I guess, is that if you take the dependent types to be discrete fibrations (but allow the base type $C$ to be an arbitrary category, i.e. not just a discrete fibration over 1), then a $C$-indexed family of categories would be a strict functor $C^{\rm op} \to \mathrm{Cat}$, which is a sort of indexed category.

Matteo Capucci (he/him) (Feb 19 2021 at 11:22):

Thanks Mike, that really clears my doubts! Indeed, I think the key was to realize I have to prescribe which functors implement 'dependency'. I guess in the case I was looking at they are fibrations, hence as you correctly point out an indexed category is just a dependent type.
Moreover, I now guess that the semantics of $\Sigma$ is the Grothendieck construction?