Universos em teoria dos tipos dependentes

Estou lendo sobre a teoria dos tipos dependentes no livro on-line da Teoria dos Tipos de Homotopia .

Na seção 1.3 do capítulo Teoria dos tipos , introduz a noção de hierarquia de Universos : , em que$\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \cdots$

todo universo é um elemento do próximo universo . Além disso, assumimos que nossos universos são cumulativos, ou seja, todos os elementos do universo também são elementos do universo .$\mathcal{U}_i$ i t h (i+1 ) t $\mathcal{U}_{i+1}$$i^{\mathrm{th}}$$(i+1)^{\mathrm{th}}$

No entanto, quando observo as regras de formação para os vários tipos no apêndice A, à primeira vista, se um universo aparece acima da barra como premissa, o mesmo universo aparece abaixo. Por exemplo, para a regra de formação de tipos de coprodutos:

$$\dfrac{\Gamma \vdash A : \mathcal{U}_i \quad \Gamma \vdash B : \mathcal{U}i}{\Gamma \vdash A + B : \mathcal{U}_i}(+\mbox{-}FORM)$$

Então, minha pergunta é por que uma hierarquia é necessária? Sob quais circunstâncias você precisa pular de um universo para outro mais alto na hierarquia? Não é realmente óbvio para mim como, dada qualquer combinação de , você pode acabar com um tipo que não está em . Em mais detalhes: as regras de formação nas seções do apêndice A.2.4, A.2.5, A.2.6, A.2.7, A.2.8, A.2.9, A.2.10, A.3.2, mencionam na premissa e julgamento, ou apenas no julgamento.$A_m: \mathcal{U}_i$$B$U$\mathcal{U}_i$$\mathcal{U}_i$

O livro também sugere que existe uma maneira formal de atribuir universos:

Se houver alguma dúvida sobre se um argumento está correto, a maneira de verificar isso é tentar atribuir níveis consistentemente a todos os universos que aparecem nele.

Qual é o processo para atribuir níveis de forma consistente?

$\mathcal{U}:\mathcal{U}$ levaria ao paradoxo de RussellU j U i j>i . Evitar o paradoxo de Russell é explicitamente mencionado no livro (página 24). Ele também entra em mais detalhes na página 54, 55, que usa “universos no estilo Russell” em vez de “universos no estilo Tarski”. Então, em um nível muito alto, tomo como certo que a teoria quer evitar o paradoxo. Infelizmente, não tenho antecedentes para entender isso diretamente. O que estou procurando nesta pergunta é realmente apenas arranhar a superfície, obtendo alguns exemplos de coisas em e não em para e pode ser qualquer outra coisa que me dê uma sensação para como as hierarquias funcionam.$\mathcal{U}_j$$\mathcal{U}_i$$j > i$

A pergunta em que circunstâncias precisamos saltar de um universo para outro mais alto na hierarquia é boa. Ter a hierarquia e a capacidade de escalá-la é importante. Você precisa pular de nível quando quiser tratar um universo como um tipo ou como parte de um tipo. Por exemplo, para definir funções do tipo (não dependente) você deve mostrar que A → U i está em um universo. Mas isso não pode ser U i ou algum universo menor. Então, o que fazemos? Para lidar com o problema (sem usar o doentio U i : U i ), precisamos saltar para cima um universo. A regra que nos permite dar esse salto é

$$A \rightarrow \mathcal{U}_i$$ $A \rightarrow \mathcal{U}_i$$\mathcal{U}_i$$\mathcal{U}_i : \mathcal{U}_i$$\mathcal{U}$-Intro No apêndice A.2.3. O ponto exato da hierarquia dos universos é que podemos fazer isso. Isso pode ser visto como uma aproximação segura da existência de universos. $$\frac{\vdash \Gamma : ctx}{\Gamma \vdash \mathcal{U}_i : \mathcal{U}_{i+1}},$$

$X : \mathcal{U}_i$$i \leq j$$X : \mathcal{U}_j$$A : \mathcal{U}_{42}$$A \to \mathcal{U}_{99}$$\to$

$$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_i}{\Gamma \vdash (X \to Y) : \mathcal{U}_i}$$ $X \to Y$$\Pi_{x : X} Y$$\Pi$$A$$\mathcal{U}_{42}$$\mathcal{U}_{99}$$\mathcal{U}_{100}$$A : \mathcal{U}_{100}$$A \to \mathcal{U}_{99}$$\mathcal{U}_{100}$

$\to$

$$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_j}{\Gamma \vdash (X \to Y) : \mathcal{U}_{\max(i,j)}}$$ $$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_j \qquad i \leq k \qquad j \leq k}{\Gamma \vdash (X \to Y) : \mathcal{U}_k}$$