Current Seminar
Homotopy Type Theory
-
David Martinez (UB):
Fonaments de la teoria homotòpica de tipus
11 March 2020, 10:30, Aula S1
Abstract:
L'objectiu d'aquesta sessió és familiaritzar-nos amb el formalisme de la teoria homotòpica de tipus. Començarem amb una breu introducció a la teoria de tipus intuïcionista i seguidament presentarem els conceptes bàsics de la versió homotòpica. -
Joachim Kock (UAB):
Univalence
Date to be announced, 10:30, Aula S1
Abstract:
TBA -
Wilson Forero (UAB):
Higher inductive types
Date to be announced, 10:30, Aula S1
Abstract:
TBA -
Xavier Ripoll (UB):
Using Agda
Date to be announced, 10:30, Aula S1
Abstract:
TBA -
Carles Casacuberta (UB):
The Blakers-Massey Theorem
Date to be announced, 10:30, Aula S1
Abstract:
TBA -
David Martinez (UB):
Coverings
Date to be announced, 10:30, Aula S1
Abstract:
TBA -
Javier J. Gutiérrez (UB):
Reflective subuniverses
Date to be announced, 10:30, Aula S1
Abstract:
TBA - Geometric uses of persistent homology (Fall 2019)
- Guest talks (Spring 2019)
- Presentable infinity categories (Fall 2018 and Spring 2019)
- Guest talks (Spring 2018)
- Homotopy types for Khovanov homology (Spring 2018)
- Fall Seminar 2017 (Fall 2017)
- Reading group on ∞-categories (Fall 2016)
- Postnikov towers and localization (Spring 2015)
- Spectral sequences (Fall 2014)
- Higher categories (Spring 2013)
- Noncommutative motives (Fall 2011)
- Spring Seminar 2011 (Spring 2011)
- Deformation theory (Fall 2010)
- Summer Seminar 2010 (Summer 2010)
- DG-categories (Spring 2010)
- Topological quantum field theories (Fall 2009)
- Quantum field theories (Fall 2009)
We plan to learn HoTT from scratch, hoping to be able to use proof assistants such as Agda or Coq and to grasp the impact of the formalism of type theory on the understanding of homotopical localizations, among other applications.
References
[1] Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, Princeton, 2013, https://homotopytypetheory.org/book/.
[2] M. Anel, G. Biedermann, E. Finster, A. Joyal, A generalized Blakers-Massey theorem, arXiv:1703.09050 (2019).
[3] U. Buchholtz, E. Rijke, The real projective spaces in homotopy type theory, arXiv:1704.05770 (2017).
[4] J. D. Christensen, M. Opie, E. Rijke, L. Scoccola, Localization in homotopy type theory,
arXiv:1807.04155 (2019).
[5] K.-B. Hou, E. Finster, D. R. Licata, P. L. Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory, arXiv:1605.03227 (2016).
[6] P. L. Lumsdaine, M. Schulman, Semantics of higher inductive types, arXiv:1705.07088 (2019).
[7] E. Rijke, M. Shulman, B. Spitters, Modalities in homotopy type theory, arXiv:1706.07526 (2019).
[8] K. Sojakova, The equivalence of the torus and the product of two circles in homotopy type theory, arXiv:1510.03918 (2015).
Past Seminars