In the usual constructions of models of type theory in ZFC set theory (including homotopical ones using model categories), we take the universes to classify the sets/spaces/objects of "cardinality" bounded by some cardinal number k. To ensure these universes are closed under both Sigma- and Pi-types, we need k to be an inaccessible [1], the existence of which is not proven by ZFC. However, ZFC does prove the existence of many cardinals with weaker closure properties. For instance, it proves there are arbitrarily large regular cardinals, and indeed arbitrarily large regular cardinals closed under powers (-)^A for any fixed A. Similarly, it proves there are arbitrarily large strong limit cardinals, and indeed arbitrarily large strong limit cardinals with any fixed cofinality. If we use these cardinals to build universes in type theory, I think we can probably obtain something like this: 1. For any universe U, there is a "regular successor universe" V such that U:V, V is closed under Sigma-types and Id-types, and V is closed under Pi-types with domain in U. 2. For any universe U, there is a "strong-limit successor universe" W such that U:W, W is closed under Pi-types (including binary product types, i.e. non-dependent Sigma-types) and Id-types, and W is closed under Sigma-types with domain in U. Has anyone studied type theory with universes like this? Or more generally type theories containing universes with weaker closure properties under type formers? And what can and can't we do in such a type theory? One thing we (apparently) can't do would be to iterate (e.g. by Nat-rec) some construction on types that sends a type X to some type that includes X in the domain of both a Sigma and a Pi. Are there naturally-occurring examples of such? There are of course definitions we use all the time that do involve a type in both the domain of a Sigma and a Pi, such as IsContr(X) = Sigma(x:X) Pi(y:X) (x=y). In this case, there is an equivalent definition of IsContr that remains in the same strong-limit universe, IsContr(X) = X * Pi(x,y:X) (x=y). Thus, we can define the h-level hierarchy by recursion on n in any strong-limit universe. Are there other such constructions that irreducibly go up a universe level, and would the resulting inability to iterate them be a problem? (Regarding HITs, in set-theoretic models I think both regular and strong-limit universes would be closed under simple ones like pushouts, and there should at least exist regular universes closed under fancier recursive HITs. Of course in homotopical models we don't yet know how to obtain even inaccessible universes closed under HITs, but we might hope that if that problem is solved then the solution would work for arbitrarily large regular universes as well. That would for instance allow us to define spheres and truncations recursively on n.) [1]: Apparently one can also construct models of *predicative* type theory in much weaker classical set theories like Kripke-Platek, with "recursive inaccessibles" used instead of actual inaccessibles. However, if we add impredicative axioms like propositional resizing, then I think the use of ZFC with true inaccessibles seems more likely to be necessary. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

In set theory there are the Zermelo universes, namely the V_\lambda for limit ordinals \lambda > \omega. They have nice closure properties in particular closure under exponentiation but what they are lacking are closure under replacement, i.e. for all A in U and f : A -> U the image of f is in U. Type theoretically this corresponds to the possibility of defining families in U by recursion over some A \in U. On the other hand in realizability models modest sets from a universe U with excellent closure properties, in particular for every A \in U and B : A -> U its sum \Sigma(A,B) \in U again. So it's very model dependent whether there exist small universes with excellent closure properties. But of course Prop or Omega is not part of such a universe. Thomas -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.