Do type constructors have type themselves?

Question

I'm recently trying to understand the basics of intuitionistic type theory, and I think I have grasped much of it. However, there is this question on my mind. For instance, can the type constructor $\to$ be regarded as an element of type $U_i\to U_i\to U_i$, where $U_i$ is some universe?

There are two main problems I can think of. First, this creates a circular reference of $\to$, which might offer the.chance of some non-normalizing construct. Second, this might cause universe inconsistencies, since $\to$ can be used with types of all universe levels.

Any help is appreciated!

Answer 1

The answer to this is pretty much, "it depends." There are generally multiple ways of presenting (roughly equivalent) type theories, and the answer might be different depending on presentation.

So, for instance, there is a way of presenting type theory in which types never themselves have a type. Instead they are just judged to be types like so:

$$Γ ⊢ A\ \mathsf{type}$$

whereas terms are judged like so:

$$Γ ⊢ e : A$$

And the way of presenting universes such that this distinction is maintained is to say that universes contain 'codes' and there is a family that 'decodes' those to the corresponding type. So:

$$\frac{}{Γ ⊢ U\ \mathsf{type}} \ \ \ \ \ \ \frac{Γ ⊢ u : U}{Γ ⊢ T(u)\ \mathsf{type}}\ \ \ \ \ \ \frac{}{Γ ⊢ \hat{ℕ} : U}\ \ \ \ \ \ T(\hat{ℕ}) = ℕ$$

and so on. This is sometimes called a Tarski style universe. But, one can also present things in a way that is called a Russell style universe, in which we just say that (some) types are themselves terms of the universe, which might have the following rules corresponding to the above:

$$\frac{}{Γ ⊢ U\ \mathsf{type}}\ \ \ \ \ \ \frac{Γ ⊢ A : U}{Γ ⊢ A\ \mathsf{type}}\ \ \ \ \ \ \frac{}{Γ ⊢ ℕ : U}$$

No computation rule being necessary, of course.

In this latter case, it might make some sense to say that something like $→$ has a type, although it might actually have many types, depending on how many universes there are. These also aren't necessarily the only ways of presenting things. Many computer implementations might more accurately be thought of as not having the $Γ ⊢ A\ \mathsf{type}$ judgment at all, and instead just talking about universes, because there are universes containing every particular type. Those would definitely rely on there being a sort of schematic type for things like $→$.

Note that there isn't exactly a circularity in these cases. For instance, if in the Russell case we say $⊢\; →\; : U → U → U$, this isn't even the initial specification of $→$, which is specified with a $\mathsf{type}$ judgment. It is just a description of which types are in $U$. If your goal were a single (non-schematic) rule that subsumed all specification of $→$, that might be more in danger of paradox, I suppose.

Answer 2

To complete the previous answer, I think in general $\to$ itself won't have a type if we take it in a very strict sense. In the proof-assistants I know, $\to$ is hard-coded in the source, as something universally defined for all universes. This is done externally to the type theory, as a computation rule.

However, you can define internally (here in Agda with HoTT, because it is what I am used to) a term $\verb!to!$ as a synonymous for $\to$ as follows :

{- OPTIONS --without-K --rewriting -}

open import HoTT

module to where

    to : ∀ {i j : ULevel} → Type i → Type j → Type (lmax i j)
    to A B = A → B

which translates basically to $\vdash\verb!to! : \Pi_{i,j}(U_i\to U_j \to U_{\operatorname{max} i, j})$.

Note that this completely eliminates the circular dependency because the type of the (internal) $\verb!to!$ is now the (external) $\to$. And we always have $\verb!to!\ A\ B = A\to B$. So saying $\to$ has type $U_i\to U_j \to U_{\operatorname{max}i,j}$ is not completely wrong if you understand it as "$\to$ is completely equivalent to a term of type $U_i\to U_j \to U_{\operatorname{max}i,j}$", even if strictly speaking, $\to$ is probably not a term in itself, and thus does not have a type