Relacionando a univalência de uma teoria de cateogrias ao conceito de esqueleto

10

Digamos que eu trabalho na teoria dos tipos de homotopia e meus únicos objetos de estudo são categorias convencionais.

Equivalências aqui são dadas por functors e G : CD que fornecem equivalências das categorias CD . Existem isomorfismos naturais α : n a t ( F G , 1 C ) e β : n a t ( G F , 1 D ), de modo que este functor e functor "inverso" sejam transformados em functor unitário.F:DCG:CD CDα:nat(FG,1C)β:nat(GF,1D)

Agora, a univalência relaciona equivalências ao tipo de identidade da teoria do tipo intencional que escolhi para falar sobre categorias. Já que eu lido apenas com categorias e essas são equivalentes se tiverem esqueletos isomórficos , gostaria de saber se posso expressar o axioma da univalência em termos de passagem para o esqueleto das categorias.C=D

Ou, caso contrário, posso definir o tipo de identidade, ou seja, a expressão sintática de uma maneira que diz essencialmente "existe um esqueleto (ou isomorfo) e C e D são equivalentes a ele".C=D:=CD

(No exposto, tento interpretar a teoria dos tipos em termos de conceitos mais fáceis de definir - as noções teóricas da categoria. Penso sobre isso porque, moralmente, parece-me que o axioma "corrige" a teoria dos tipos intencionais por meio de códigos codificados o princípio da equivalência , que já é uma parte natural da formulação dos enunciados teóricos da categoria, por exemplo, especificar objetos apenas em termos de propriedades universais.)

Nikolaj-K
fonte
2
Você leu o capítulo 9 do livro HoTT? É sobre teoria das categorias.
Andrej Bauer

Respostas:

11

Refiro-lhe o capítulo 9 do livro HoTT. Em particular, uma categoria é definida de tal forma que os objetos isomórficos são iguais, consulte a Definição 9.1.6 . Como o Exemplo 9.1.15 aponta, realmente não existe uma noção razoável de "esquelética" no HoTT. Isso ocorre porque a igualdade é tão fraca que já significa "isomórfica".

Além disso, o Teorema 9.4.16 diz

AB

(A=B)(AB)

O teorema nos diz que o axioma da univalência nos dá uma espécie de sonho do teórico cateórico: categorias equivalentes são iguais.

10

Andrej Bauer
fonte