Una visión general del axioma de univalencia en teoría de tipos homotópica
Plática dada por Marco Federico Larrea Schiavon (Facultad de Ciencias de la UNAM) en el Primer Encuentro de Computación Teórica el viernes 7 de diciembre del 2018 en el Anfiteatro Alfredo Barrera del conjunto Amoxcalli, Facultad de Ciencias de la UNAM.
Video proporcionado por Ciencias TV
Video en Facebook
https://www.facebook.com/Ciencias.TV/videos/2329947740362148/
Video en Youtube
https://youtu.be/lQvM4kU1BZY
Resumen:
La Teoría de Tipos Homotópica (HoTT por sus siglas en inglés) es un lenguaje formal que consiste de objetos primitivos llamados tipos y de algunas reglas para manipularlos. Desde un punto de vista semántico, los tipos pueden ser considerados como espacios topológicos desde una perspectiva homotópica. Esto significa que en el lenguaje de HoTT solo podremos hablar sobre propiedades homotópicas de espacios como, por ejemplo, trayectorias y homotopías. El Axioma de la Univalencia es un fortalecimiento adicional de HoTT propuesto por Vladimir Voevodsky. En pocas palabras, nos permite caracterizar el tipo de trayectorias entre dos tipos como el tipo de equivalencias entre ellos. Esto resulta ser una adición muy poderosa y útil a HoTT. En esta ponencia, daré una breve introducción a HoTT sin profundizar en los detalles sintácticos. Después de esto, daré una declaración formal del Axioma de la Univalencia y discutiremos algunas de sus implicaciones. No se requieren conocimientos previos de lógica ni de Teoría de Tipos. Sin embargo, me basaré en algunas nociones básicas de los espacios topológicos y de Teoría de Homotopía para guiar la intuición.
Pagina del Primer Encuentro de Computación Teórica
https://sites.google.com/ciencias.unam.mx/papime102117/encuentro
Marco Federico Larrea Schiavon en:
Facultad de Ciencias de la UNAM:
http://www.fciencias.unam.mx/directorio/60008
Agradecemos el apoyo de:
universo.math
http://universo.math.org.mx/
https://www.facebook.com/universo.math
Departamento de Matemáticas del CINVESTAV
http://www.math.cinvestav.mx/
Facultad de Ciencias de la UNAM
http://www.fciencias.unam.mx/
Sociedad Matemática Mexicana
https://www.facebook.com/SociedadMatematicaMexicana/
La banda que coopero en la vaquita para reponer el equipo que nos robaron en noviembre del 2017
https://www.facebook.com/Ciencias.TV/videos/426024461479542/
Siguenos en:
Página de Facebook de Ciencias TV:
https://www.facebook.com/Ciencias.TV
Página web:
http://cienciastv.org.mx
Ciencias TV – Matemáticas
https://www.facebook.com/Ciencias-TV-Matem%C3%A1ticas-106574140723552/
Ciencias TV – Física
https://www.facebook.com/Ciencias-TV-F%C3%ADsica-115341676509427/
Ciencias TV – Biología y Ambiente
https://www.facebook.com/Ciencias-TV-Biolog%C3%ADa-y-Ambiente-111565396888097/
Telegram:
t.me/cienciastv
@cienciastv
Twitter:
@Ciencias_TV
Instagram:
@ciencias.tv
Youtube
https://www.youtube.com/channel/UCAvg7yOE4-25TPDUeKFUztA
Lista de reproducción con los videos que hemos publicado:
https://www.youtube.com/playlist?list=PLiD-IJzweXR9CMW8piN4Pf1HjgSiGjLyi