타입 유니버스

타입 유니버스(type universe)는 타입들의 타입이다.

정의 방식

러셀 스타일 유니버스

러셀 스타일에서는 유니버스 \(\newcommand{\univ}[0] {\mathcal{U}} \univ\)에 속하는 대상이 곧 타입이다. \[ \newcommand{\type}[1] {#1 \ \text{type}} \type{\univ} \qquad \begin{prooftree} \AXC{$A : \univ$} \UIC{$\type{A}$} \end{prooftree} \]

타르스키 스타일 유니버스

타르스키 스타일에서 유니버스 \(\univ\)에 속하는 대상들은 타입의 부호(code)이며, 이 부호에 대응하는 타입을 주는 함수 \(\mathcal{T}\)가 함께 주어진다. \[ \type{\univ} \qquad \begin{prooftree} \AXC{$\check A : \univ$} \UIC{$\type{\mathcal{T}(\check A)}$} \end{prooftree} \]

유니버스 계층

아래 내용은 러셀 스타일을 따라 서술하였다. 유니버스 타입 \(\univ\)가 들어가는 유니버스가 필요하다면, \(\univ\)보다 큰 새로운 유니버스 \(\univ'\)이 필요하다. 그러나 \(\univ'\)이 들어가는 유니버스가 필요한 경우, 이보다 더 큰 또 다른 유니버스 \(\univ''\)을 도입해야 한다. 이와 같은 과정을 무한히 반복하면 다음과 같은 유니버스 계층(universe hierarchy)이 얻어진다. \[ \begin{array}{c} \univ_0 : \univ_1 \\ \univ_1 : \univ_2 \\ \univ_2 : \univ_3 \\ \vdots \end{array} \]

누적성

러셀 스타일 유니버스 계층을 갖춘 타입이론에서 누적성(cumulativity)은 다음을 가리킨다. \[ \begin{prooftree} \AXC{$A : \univ_i$} \UIC{$A : \univ_{i+1}$} \end{prooftree} \] 누적성은 타입이론을 사용하기 편리하게 만들어주지만, 타입의 유일성이 성립하지 않게 만든다.