Relation Between Dependent Type Theory And Categories I have been trying to understand the relationship between a dependent type theory and a corresponding locally Cartesian closed category $\mathbb C,$ as described in
R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95
But I am having some difficulty. As I understand it, the objects of $\mathbb C$ are types without free variables, and the arrows of $\mathbb C$ are members of independent function types.
If $\mathbb U$ denotes a universe of types, then am I correct in thinking that a type family $B: A \rightarrow \mathbb U$ corresponds to a (projection) function $\pi _1 : \Sigma _{x:A} B(x) \rightarrow A$ ? It seems that the above reference states that this type family $B$ also corresponds a member of the slice category $\mathbb{C} / A.$ I am trying to understand this. I guess that a type family $B$ corresponds to an object of $\mathbb{C} / A$ because $B$ corresponds to an arrow $\pi _1 : \Sigma _{x:A} B(x) \rightarrow A$ of $\mathbb C,$ that goes into $A$ (and the objects of the slice category $\mathbb{C} / A$ correspond to arrows of $\mathbb C,$ that go into $A$).
I would appreciate it if somebody could tell me if I am on the right track with this thinking.
The other thing I am very confused about is that the dependent type theory described in the homotopy type theory book I read had a hierarchy of universes $\mathbb U _0 : \mathbb U _1 ,$ and $\mathbb U _1 : \mathbb U _2 , \dots$ etc. I am confused about how these universes interplay with the correspondance between the type theory and the locally Cartesian closed category described above ? I presume there is no object of $\mathbb C$ which actually corresponds to a type universe in the theory, but it would be great if somebody could explain more about how type universes enter into the correspondence (if they do).
 A: 
As I understand it, the objects of ℂ are types without free variables, and the arrows of ℂ are members of independent function types.

This is right, to first approximation.  Technically it's better to take the objects of $\mathbb{C}$ to be contexts, but in a theory with $\Sigma$-types satisfying a uniqueness/eta rule every context is isomorphic to a single closed type, so the first-approximation answer gives an equivalent category.
A type universe is itself a type, hence an object of this category, and so a type family $B:A\to \mathbb{U}$ is at its most basic level just a morphism in the category.  There is also the projection function $\pi_1 : (\sum_{x:A} B(x)) \to A$ as you say, which is an object of the slice category $\mathbb{C}/A$, and the correspondence between them is that $\pi_1$ is the pullback along $B$ of the universal projection $\pi_1 : (\sum_{X:\mathbb{U}} X) \to \mathbb{U}$.  So yes, you are basically on the right track here too.
The deal with hierarchies of universes is just that in a consistent theory it can't be that every type is an element of the same universe $\mathbb{U}$, or put categorically it can't be that every object of $\mathbb{C}/A$ is classified by some map $B:A\to \mathbb{U}$ for the same $\mathbb{U}$.  Each type universe in the hierarchy yields an object of the category that classifies some, but not all, of the objects of each slice category.
