Submitted by Natalia de Souza Gonçalves (natalia.goncalves@ufpe.br) on 2015-05-08T13:12:46Z
No. of bitstreams: 2
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
dissertation.pdf: 1398032 bytes, checksum: ba6c27cf093110dd1dcf9fea1b529c41 (MD5) / Made available in DSpace on 2015-05-08T13:12:46Z (GMT). No. of bitstreams: 2
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
dissertation.pdf: 1398032 bytes, checksum: ba6c27cf093110dd1dcf9fea1b529c41 (MD5)
Previous issue date: 2014-02-27 / CNPq / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/13853 |
| Date | 27 February 2014 |
| Creators | Silva Júnior, João Alves |
| Contributors | Queiroz, Ruy José Guerra Barreto de |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.002 seconds