topology@ub

Research Group in Algebraic Topology

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).