[HoTT] regular and strong-limit universes

[Michael Shulman <shulman@sandiego.edu>]

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.