Slice categories and dependent types

Question

How are slice categories related to dependent types ? Here is a quote from Mclarty's book Elementary Categories, Elementary Toposes that made me wonder about this:

high-level programming languages have dependent types, data types which themselves depend on parameters in other data types.

So I am wondering what the general connection is. An example in Idris would be great, but not necessary.

Answer 1

One can model a dependent type theory in a locally cartesian closed category $\mathcal{C}$:

• A closed type is interpreted as an object;
• A term is interpreted as a morphism;
• A dependent type upon $X$ is interpreted as an object of the slice category $\mathcal{C}/X$.

Substitution of terms in types is interpreted as a pullback between the slices of C.

This was proposed by Seely in his seminal paper Locally cartesian closed categories and type theory.