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).


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.

  • $\begingroup$ Thanks. The Seely paper makes a lot of connections, and your answer has helped me to start to understand it. $\endgroup$ Dec 6 '20 at 11:15
  • 1
    $\begingroup$ If you'll forgive a bit of self-promotion, my paper the logic of space is another reference that sketches the categorical interpretation of type theories at a high level. $\endgroup$ Dec 6 '20 at 18:34
  • $\begingroup$ That sounds like an excellent recommendation. I look forward to checking it out. $\endgroup$ Dec 7 '20 at 21:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.