Examples of the categorical interpretation of dependent types I'm trying to understand the correspondence between dependent types and category theory.                              
Let me tell you about my current (I admit, limited) knowledge on the two topics...
On the category theory side – following this exercise (problems 4-8), I know that:       


*

*The slice category $\mathbf{Set}/I$ is equivalent to the $I$-indexed category $\mathbf{Set}^I$.                     

*For any morphism $f : J \to I$ in $\mathbf{Set}$ we can construct a functor that "changes the base" $f^* : \mathbf{Set}/I \to \mathbf{Set}/J$.

*The functor $f^*$ is right adjoint to $f_! : \mathbf{Set}/J \to \mathbf{Set}/I$.                                     

*The functor $f_!$ corresponds to the disjoint union operator when $I = 1$.                         


On the dependent types side – I have only a cursory understanding, mostly through examples.
To enumerate a couple: 


*

*The set of vectors indexed by their size.

*The set of triples $(a, b, p)$ where $a$ and $b$ are numbers and $p$ is a proof that $a \le b$.


My question is on how to interpret examples like these in a categorical setting:


*

*What do dependent types correspond to in a categorical setting?

*Conversely, what do the various categorical objects (slice category, index set, functors that "change the base") correspond to in terms of dependent types?

 A: One thing to mention is that the individual slice categories can be assembled together into one structure, the arrow category $\mathbf{Set}^\to$. Every object of $\mathbf{Set}/I$ is an object of $\mathbf{Set}^\to$, the maps in $\mathbf{Set}/I$ form part of a map in $\mathbf{Set}^\to$, because the latter are commutative squares, and the map in $\mathbf{Set}/I$ forms a commutative square when paired with the identity function on $I$. But, the arrow category also has maps that mediate between objects that would have to be in different slice categories, because the square can pair the reindexing from $I$ to $J$ with the maps between the indexed families that respect the reindexing.
This 'whole structure' view forms part of the "codomain fibration", where we have a functor $\mathbf{Set}^\to \to \mathbf{Set}$ sending each arrow to its codomain, or each indexed family to its indexing set. Then the $f^*$ and $f_!$ functors can be talked about with respect to this structure, and it forms a more general setting for modelling (among other things) dependent types. You can consider fibrations that aren't particular to $\mathbf{Set}$ for instance, which gives one way of making sense of dependent types in more general categories.
The answer to your first question is that there is no specific encoding, I think. There are multiple ways of thinking about each type, and they are useful for thinking about different aspects of those types. For instance, your first example is vectors indexed by their size. In type theory notation, this might be:
$$n : ℕ ⊢ \mathsf{Vec} \; n \;\; \mathsf{type}$$
(I'm assuming there's some particular type, say integers, for the elements of the list). One way to think about this is to just take this to be the map:
$$length : List → ℕ$$
where $List$ is the set of lists of integers, which makes up the 'total space' representing the values of our type family $\mathsf{Vec}\; n$. However, we can also think of things in an indexed way, where we have something like:
$$Vec : ℕ → \mathcal{P}(List)$$
where $Vec$ is a function that maps natural numbers to the subset of lists of integers with that length. This is how we often think of things internally to type theory. Now, given this function, we can reconstruct the total space like so:
$$\int Vec = \{(n:ℕ, l) \mid l \in Vec(n)\} $$
and there is a map:
$$ π_1 : \int Vec \to ℕ$$
which just projects out the first part of the pair.
So, the reason to think in these two different ways is that they each make one of the $f$ operations kind of trivial, and the other more complicated. In the first case, $f_!$ is just post-composition, changing the reported index of the values of the total space. The total space itself doesn't change at all. However, $f^*$ is pullback, which is kind of non-obvious. It produces a new total space with a mapping to $J$ that forms a pullback square with $List$, $length$ and $f : J \to ℕ$.
In the other case, $f^*$ seems more trivial. It is just composing $f$ with $Vec$ to create a new mapping function. On the other hand, $f_!$ is complicated, and similar to the definition of the total space. If we have $f : ℕ \to J$, then:
$$(f_!Vec) j = \{ l \mid n \in ℕ, f(n) = j, l \in Vec(n)\}$$
Note that for $! : ℕ \to 1$, $!_! = \int$.
This latter view is fairly similar to how things are presented in type theory, though, so it's a pretty good guide for how things map from the categorical/fibered presentation to type theory syntax. An object in a slice category $\mathbf{Set}/I$ is a type in a context:
$$i : I ⊢ T \; \mathsf{type}$$
"Change of base" corresponds to 'precomposition' with a family, which involves substitution in the notation I'm using:
$$\frac{i : I ⊢ T \; \mathsf{type}}{j : J ⊢ T[i := f(j)] \mathsf{type}}$$
The $f_!$ operation corresponds to the $Σ$ type, although the categorical version is generalized in an inconvenient way. The simple correspondence to type theory is to consider maps like $fst : Γ × J \to Γ$. Then $fst_! : \mathbf{Set}/(Γ×J) \to \mathbf{Set}/Γ$ is written as:
$$\frac{Γ, j : J ⊢ T \; \mathsf{type}}{Γ ⊢ \Sigma_{j:J} T \; \mathsf{type}}$$
Making sense of the categorical version involves constructing inverse images, which is sort of the inverse of the $\int$ construction, although it can be done.
I think the last thing to cover is the $a \leq b$ example, but that has similar ways to think about it. The only 'complicated' part is thinking about the 'proofs'. The $Vec$ alike way says that the $p$ belong to a family ${\leq} : ℕ × ℕ \to \mathcal{P}1$, where $m \leq n$ is empty if $m$ is greater than $n$ or a singleton otherwise (that description is potentially overly simple in general). The opposite view is that the total space of the family is the subset of $\leq \; \subset ℕ × ℕ$ where the first element is less than or equal to the second, and the object in $\mathbf{Set}/(ℕ×ℕ)$ is just the inclusion map. Then the 'triples' are just composing this with the terminal map $! : ℕ×ℕ \to 1$ (or doing it in two steps if you prefer).
Hopefully this was clear enough. I can try to fix it if something isn't.
