Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.ufpe.br/handle/123456789/13853
Title: First steps in homotopy type theory
Authors: Silva Júnior, João Alves
Keywords: Teoria homotópica de tipos;Fundamentos univalentes;Grupo fundamental do círculo;Lema do achatamento;Cobertura universal do círculo
Issue Date: 27-Feb-2014
Publisher: Universidade Federal de Pernambuco
Abstract: 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.
URI: https://repositorio.ufpe.br/handle/123456789/13853
Appears in Collections:Dissertações de Mestrado - Matemática

Files in This Item:
File Description SizeFormat 
dissertation.pdf1.37 MBAdobe PDFView/Open


This item is protected by original copyright



This item is licensed under a Creative Commons License Creative Commons