Please use this identifier to cite or link to this item: http://hdl.handle.net/2445/165004
Title: Teoria homotòpica de tipus
Author: Martínez Carpena, David
Director/Tutor: Casacuberta, Carles
Keywords: Teoria de l'homotopia
Treballs de fi de grau
Tor (Geometria)
Àlgebra homològica
Lògica informàtica
Homotopy theory
Bachelor's theses
Torus (Geometry)
Homological algebra
Computer logic
Issue Date: 19-Jan-2020
Abstract: [en] Homotopy type theory is a branch of mathematics that emerged in the decade of 2010. The major novelties with respect to previous type theories are the association of types with $\infty$ -groupoids, Voevodsky’s univalence axiom, and higher-order inductive types. Higher- order inductive types allow certain objects to be defined, such as a circle or a torus, in a synthetic way. The first chapters of this work offer an introduction to homotopy type theory, focusing especially on understanding higher-order inductive types. Due to the short time elapsed since the advent of homotopy type theory, there are many open questions waiting to be answered. This work sets out a research direction motivated by one of these questions: how to find an appropriate definition of orientability which is meaningful for surfaces or, more generally, for manifolds. From the existing definition of a torus as a higher-order inductive type, we have studied an analogous definition of a Klein bottle, focusing on the fact that a torus is a two-sheeted covering of a Klein bottle. This work contains basic facts about coverings in homotopy type theory, as well as a few results that are relevant in the special case of the torus and the Klein bottle.
Note: Treballs Finals de Grau de Matemàtiques, Facultat de Matemàtiques, Universitat de Barcelona, Any: 2020, Director: Carles Casacuberta
URI: http://hdl.handle.net/2445/165004
Appears in Collections:Treballs Finals de Grau (TFG) - Matemàtiques

Files in This Item:
File Description SizeFormat 
165004.pdfMemòria626.26 kBAdobe PDFView/Open


This item is licensed under a Creative Commons License Creative Commons