1
$\begingroup$

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

$\endgroup$

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Thanks. The Seely paper makes a lot of connections, and your answer has helped me to start to understand it. $\endgroup$ Dec 6, 2020 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, 2020 at 18:34
  • $\begingroup$ That sounds like an excellent recommendation. I look forward to checking it out. $\endgroup$ Dec 7, 2020 at 21:58

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .