Homotopy type theory
We planned 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.
The seminar was cancelled due to Covid-19.
-
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
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).