First steps in homotopy type theory

• Ano de defesa: 2014
• Autor(a) principal: Silva Júnior, João Alves
• Orientador(a): Queiroz, Ruy José Guerra Barreto de
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Universidade Federal de Pernambuco
• Palavras-chave em Português: Teoria homotópica de tipos; Fundamentos univalentes; Grupo fundamental do círculo; Lema do achatamento; Cobertura universal do círculo
• Link de acesso: https://repositorio.ufpe.br/handle/123456789/13853

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.