3
$\begingroup$

A type universe is a type of small types that is closed under the basic type formation operations (dependent product, sum, coproduct etc.), that is to say for example that from

  • $A \colon U_i$ and
  • $x \colon A \vdash B[x] \colon U_i$

derive $\prod(x\colon A).B[x] \colon U_i$.

I haven't yet found anything in my reading that discusses the effects of having

  • $\prod(x\colon A).B[x] \colon U_i$,
  • $A \colon U_{i+1}$ and
  • $x \colon A \vdash B[x] \colon U_{i+1}$

derivable, but $A \colon U_i$ and $x \colon A \vdash B[x] \colon U_i$ not derivable.

Does anything interesting arise if we require the converse of type formation rules to hold, and add in "type formation conditions" stating e.g. "from $\prod(x\colon A).B[x] \colon U_i$ derive $A \colon U_i$" (or similar things for other types)?

N.B. I've been thinking about this in the setting of Russell-style universes, and am equally unsure what happens in Tarski-style universes.

Edit --- I have just realized that my question is somewhat silly in the usual context, where typing judgments are made in the presence of type contexts for variables, which requires one to derive $A \colon U_i$ etc. before being able to derive $\prod(x\colon A).B[x] \colon U_i$. I am however currently working in a different formulation which needs a bit more explaining, and so I'll add more information soon.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ Taken literally this would imply that your universe is everything - say if one of the $B[x]$ is empty $\endgroup$
    – მამუკა ჯიბლაძე
    Commented Jul 17, 2018 at 9:42
  • $\begingroup$ After some additional thought, I think the point is that the theory is normally set up so that in order to even derive $\prod(x\colon A).B[x] \colon U_i$ in the first place, one needs to have a well-formed context, in which $A \colon U_i$ has already been derived. Thus usually the rule I suggest is already a meta-theorem. $\endgroup$
    – Josh
    Commented Jul 17, 2018 at 10:08
  • 2
    $\begingroup$ @მამუკაჯიბლაძე Not really. If one of the $B[x]$ is empty, then the type $\prod(x:A).B[x]$ will also "be empty" in the sense of having no elements, but it will not be definitionally identical to "the empty type", so we cannot automatically conclude from this that it belongs to $U_i$. $\endgroup$
    – Mike Shulman
    Commented Jul 23, 2018 at 4:32

1 Answer 1

Reset to default
4
$\begingroup$

I expect you're right that if the only primitive rules for universes are "closure" ones such as

$$\frac{\vdash A:U_i \qquad x:A \vdash B[x] : U_i}{\vdash \prod(x:A). B[x] : U_i}$$

then there should be a metatheorem that whenever $\prod(x:A). B[x] : U_i$ it must have been derived by this rule so that we have $A:U_i$ and $x:A \vdash B[x] : U_i$ as well. (Such metatheorems are generally quite a lot of work to actually prove, so I hesitate to assert that there is such a theorem, but it seems plausible to me.)

However, there are type theories containing primitive rules allowing types in smaller universes to be built out of types in bigger ones. Probably the most well-known of these is asking for a small universe such as $U_0$ to be "impredicative" in the sense that it is closed under products of arbitrarily sized domain:

$$\frac{\vdash A:U_i \qquad x:A \vdash B[x] : U_0}{\vdash \prod(x:A). B[x] : U_0}$$

For instance, in the Predicative Calculus of Inductive Constructions that underlies the Coq proof assistant, the universe Prop is impredicative in this sense. The impredicative Calculus of Inductive Constructions, which can be turned on by the option --impredicative-set, also includes another impredicative universe Set, although these are "parallel" rather than "sequential" (that is, we have Prop : Type1 and Set : Type1 but not Prop : Set) --- I believe it is known to be inconsistent to have one impredicative universe containing another impredicative universe, although two "parallel" impredicative universes are known to be consistent (relative to standard set theory).

Vladimir Voevodsky suggested another class of "bigger into smaller" universe rules that he called "resizing rules", and which can be described generally by "adding extra useless junk to a type shouldn't raise its universe level". For instance, one such rule is that if $A:U_i$ and $B : U_j$ for $j>i$, while $A\simeq B$ (an equivalence/isomorphism of types), then $B:U_i$. Another is that if $A:U_i$ and $A$ is a subsingleton (i.e. $\prod(x:A)(y:A). x=y$), then $A:U_0$. As far as I know, none of these rules are known to be consistent.

A general framework for describing and studying type theories containing families of "universes" (not necessarily sequentially ordered) with arbitrarily chosen universe-assignments for the types in the $\prod$-formation rule is pure type systems. A PTS is specified by a set of sorts (the universes), a set of axioms of the form $s_1:s_2$ for sorts $s_1,s_2$ (specifying which universes belong to which others), and a set of rules of the form $(s_1,s_2,s_3)$ each specifying a way to assign universes to the types in $\prod$-formation:

$$\frac{\vdash A:s_1 \qquad x:A \vdash B[x] : s_2}{\vdash \prod(x:A). B[x] : s_3}$$

PTS's are very general and include even the inconsistent theory $U:U$.

Improve this answer
$\endgroup$

You must log in to answer this question.

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