Título:

First Steps in Homotopy Type Theory

Autor:

JOAO ALVES SILVA JUNIOR

Tipo de Trabalho de Conclusão:

DISSERTAÇÃO

Abreviatura:

JÚNIOR, J. A. S.

Data da Defesa:

27/02/2014

Resumo:

Em abril de 2013, o Programa de Fundamentos Univalentes do IAS, Princeton, lançou o primeiro livro em teoria homotópica de tipos, apresentando várias provas de resultados da teoria da homotopia em “um novo estilo de ‘teoria de tipos informal’ que pode ser lida e entendida por um ser humano, como um complemento à prova formal que pode ser checada por uma máquina”. O objetivo desta dissertação é dar uma abordagem mais detalhada e acessível a algumas dessas provas. Escolhemos como leitmotiv uma versão tipoteórica (originalmente proposta por Michael Shulman) de uma prova padrão de 1(S1) = Z usando espaços de recobrimento. Um ponto crucial dela é o uso do “lema do achatamento” (flattening lemma), primeiramente formulado em generalidade por Guillaume Brunerie, cujo enunciado é bem complicado e cuja a prova é difícil, muito técnica e extensa. Enunciamos e provamos um caso particular desse lema, restringindo-o à mínima generalidade exigida pela demonstração de 1(S1) = Z. Também simplificamos outros resultados auxiliares, adicionamos detalhes a algumas provas e incluímos algumas provas originais de lemas simples como “composição de mapas preserva homotopia”, “contrabilidade é uma invariante homotópica”, “todo mapa entre tipos contráteis é uma equivalência”, etc.

Palavras-chave:

Palavras-chaves: teoria homotópica de tipos. fundamentos univalentes. grupo fundamental do círculo. lema do achatamento. cobertura universal do círculo.

Abstract:

In April 2013, the Univalent Foundations Program, IAS, Princeton, released the first book on homotopy type theory, presenting several proofs of results from homotopy theory in “a new style of ‘informal type theory’ that can be read and understood by human beings, as a complement to a formal proof that can be checked by a machine.” The objective of this dissertation is to give a more detailed and accessible approach to some of these proofs. We have chosen as leitmotif a type-theoretic version (originally proposed by Michael Shulman) of a standard proof of 1(S1) = Z using covering spaces. A crucial point of it is the use of the flattening lemma, firstly formulated in generality by Guillaume Brunerie, whose statement is very complicated and whose proof is difficult, very technical and extensive. We state and prove a particular case of this lemma, restricting it to the minimum generality required by the proof of 1(S1) = Z. We also simplify other auxiliary results, add missing details to some proofs, and include some original proofs of simple lemmas such as “composition of maps preserves homotopy,” “contractibility is a homotopy invariant,” “every map between contractible types is an equivalence,” etc.

Keywords:

Keywords: homotopy type theory. univalent foundations. fundamental group of the circle. flattening lemma. universal cover of the circle.

Volume:

1

Páginas:

58

Idioma:

INGLES

Biblioteca depositada:

Central e Setorial

Autorização de divulgação:

O trabalho não possui divulgação autorizada

Área de Concentração:

ANÁLISE

Linha de Pesquisa:

LÓGICA MATEMÁTICA, TEORIA DA COMPUTAÇÃO, E FUNDAMENTOS DA SEGURANÇA COMPUTACIONAL

Projeto de Pesquisa:

PROJETOS MEDLAR I, E MEDLAR II

Orientador:

RUY JOSE GUERRA BARRETTO DE QUEIROZ

O orientador principal compôs a banca do discente?:

Não

Tipo de Vínculo Empregatício:

Servidor Público

Tipo de Instituição:

Instituição de Ensino e Pesquisa

Expectativa de Atuação:

Ensino e Pesquisa

Mesma Área de Atuação?

Sim