8
$\begingroup$

I know that locally closed cartesian categories provide categorical semantics for type theories with dependent products.

What kind of categories model type theories with infinite universe hierarchies (cumulative or non-cumulative)?

$\endgroup$
2
  • $\begingroup$ What are you assuming about the universes? Just closure under $\Pi$? $\endgroup$
    – David Roberts
    May 1, 2021 at 1:37
  • 5
    $\begingroup$ At an elementary level, there isn't going to be an answer to this other than something like "LCCs with universes". More interestingly, there are non-elementary ways to construct universes, e.g. in Grothendieck toposes if there are inaccessible cardinals in the ambient set theory. Is that the sort of thing you're interested in? $\endgroup$ May 1, 2021 at 2:11

1 Answer 1

4
$\begingroup$

A universe in a category with display maps is a specified display map $\tilde U \to U$ (cf. Section 5.5 of Taylor's thesis Recursive Domains, Indexed Category Theory and Polymorphism, or Section 9.6 of Taylor's Practical Foundations of Mathematics; the notation in this answer follows Voevodsky's A C-system defined by a universe in a category). Recall that objects represent contexts, and display maps represent projections from extended contexts, and so this display map can be interpreted as a term $X : U, x : X \vdash X : U$. We can extend a context $\Gamma$ by a $U$-small type $A$ (that is, a type in the universe $U$) by taking a pullback along the universe:

extending a context

The morphism $\Gamma, a : A \to \tilde U$ is viewed as picking out the type $A$ and the term $a : A$. Conversely, any display map $\Gamma, a : A \to \Gamma$ that fits into a pullback square along the universe may be seen as an extension by a $U$-small type in this way.

We can therefore define a hierarchy of (non-cumulative) universes to be a family of display maps $\{ \tilde U_i \to U_i \}_{i \in \mathbb N}$ such that each $U_i$ is $U_{i + 1}$-small. One may additionally want to impose axioms on these universes asserting that they are closed under the type constructors appropriately.

Modulo coherence issues, a locally cartesian-closed category is a display map category, and so dependent type theories with dependent sums, dependent products, extensional identity types and universes are modelled by locally cartesian-closed categories with universes. (Mike Shulman points this out in the comments, but it's surprisingly difficult to find a definition of universe in this setting, so I thought it would be helpful to spell out.)

$\endgroup$
3
  • 3
    $\begingroup$ Somebody introduced categories with display maps and this definition of universes in his thesis in 1987. $\endgroup$ May 6, 2021 at 19:16
  • $\begingroup$ @PaulTaylor: I should have thought to look there, thanks! I shall add a reference imminently. $\endgroup$
    – varkor
    May 6, 2021 at 19:21
  • $\begingroup$ For categories with display maps, Chapter VIII of my book is a much better account. For universes, the Andy Pitts' paper on Russell's paradox that also has my name on it, is probably the best early reference. $\endgroup$ May 10, 2021 at 18:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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