topology@ub

Research Group in Algebraic Topology

Current Seminar

Homotopy Type Theory

    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.

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


    Past Seminars